diff --git a/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml b/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml
index 9d3200a693a..44af2a46cfc 100644
--- a/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml
+++ b/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml
@@ -300,6 +300,7 @@ let parse_fstar_incrementally
 : FStarC_Parser_AST_Util.extension_lang_parser 
 = let f =
     fun (s:string) (r:FStarC_Compiler_Range.range) ->
+      let open FStar_Pervasives in
       let open FStarC_Compiler_Range in
       let lexbuf =
         create s
@@ -324,7 +325,7 @@ let parse_fstar_incrementally
             FStarC_Parser_Parse.oneDeclOrEOF
         in
         match err_opt with
-        | None -> FStar_Pervasives.Inr decls
+        | None -> Inr decls
         | Some (_, msg, r) -> 
           let open FStarC_Parser_AST in
           let err_decl = mk_decl Unparseable r [] in
diff --git a/ocaml/fstar-lib/FStarC_Reflection_Types.ml b/ocaml/fstar-lib/FStarC_Reflection_Types.ml
index cb3382fdd32..f0a3c0a42da 100644
--- a/ocaml/fstar-lib/FStarC_Reflection_Types.ml
+++ b/ocaml/fstar-lib/FStarC_Reflection_Types.ml
@@ -1,3 +1,4 @@
+open FStar_All
 
 (* TODO: make this an F* module, no need to drop to OCaml for this *)
 
diff --git a/ocaml/fstar-lib/FStar_Reflection_Typing_Builtins.ml b/ocaml/fstar-lib/FStar_Reflection_Typing_Builtins.ml
index 49c1f5bd1a5..1a0e98d571b 100644
--- a/ocaml/fstar-lib/FStar_Reflection_Typing_Builtins.ml
+++ b/ocaml/fstar-lib/FStar_Reflection_Typing_Builtins.ml
@@ -1,4 +1,5 @@
 open FStarC_Syntax_Syntax
+open FStarC_Reflection_Types
 module R = FStarC_Compiler_Range
 
 let dummy_range = R.dummyRange
diff --git a/tests/semiring/CanonCommSemiring.ml.fixup b/tests/semiring/CanonCommSemiring.ml.fixup
index e878dced53d..02da1deab67 100644
--- a/tests/semiring/CanonCommSemiring.ml.fixup
+++ b/tests/semiring/CanonCommSemiring.ml.fixup
@@ -3,7 +3,7 @@
 (* This is needed since we have no automatic embeddings for Tac functions, but we
 should add them *)
 let _ =
-  FStar_Tactics_Native.register_tactic "CanonCommSemiring.canon_semiring_aux"
+  FStarC_Tactics_Native.register_tactic "CanonCommSemiring.canon_semiring_aux"
     (Prims.parse_int "11")
     (fun psc  ->
       fun ncb ->
@@ -11,22 +11,22 @@ let _ =
           fun args  ->
             match args with
             | (tv_0,_)::args_tail ->
-                (FStar_Tactics_InterpFuns.mk_tactic_interpretation_9
+                (FStarC_Tactics_InterpFuns.mk_tactic_interpretation_9
                    "CanonCommSemiring.canon_semiring_aux (plugin)"
-                   (FStar_Tactics_Native.from_tactic_9 canon_semiring_aux)
-                   FStar_Reflection_V2_Embeddings.e_term
-                   (FStar_Tactics_Interpreter.e_tactic_1_alt
-                       FStar_Reflection_V2_Embeddings.e_term
-                       (FStar_Syntax_Embeddings.mk_any_emb tv_0))
-                   (FStar_Tactics_Interpreter.e_tactic_1_alt
-                       (FStar_Syntax_Embeddings.mk_any_emb tv_0)
-                       FStar_Reflection_V2_Embeddings.e_term)
-                   FStar_Reflection_V2_Embeddings.e_term
-                   FStar_Reflection_V2_Embeddings.e_term
-                   FStar_Reflection_V2_Embeddings.e_term
-                   FStar_Reflection_V2_Embeddings.e_term
-                   FStar_Reflection_V2_Embeddings.e_term
-                   FStar_Syntax_Embeddings.e_any
-                   FStar_Syntax_Embeddings.e_unit
+                   (FStarC_Tactics_Native.from_tactic_9 canon_semiring_aux)
+                   FStarC_Reflection_V2_Embeddings.e_term
+                   (FStarC_Tactics_Interpreter.e_tactic_1_alt
+                       FStarC_Reflection_V2_Embeddings.e_term
+                       (FStarC_Syntax_Embeddings.mk_any_emb tv_0))
+                   (FStarC_Tactics_Interpreter.e_tactic_1_alt
+                       (FStarC_Syntax_Embeddings.mk_any_emb tv_0)
+                       FStarC_Reflection_V2_Embeddings.e_term)
+                   FStarC_Reflection_V2_Embeddings.e_term
+                   FStarC_Reflection_V2_Embeddings.e_term
+                   FStarC_Reflection_V2_Embeddings.e_term
+                   FStarC_Reflection_V2_Embeddings.e_term
+                   FStarC_Reflection_V2_Embeddings.e_term
+                   FStarC_Syntax_Embeddings.e_any
+                   FStarC_Syntax_Embeddings.e_unit
                    psc ncb us) args_tail
             | _ -> failwith "arity mismatch")