Update manual ml fixup file for new internals

FStarLang · Oct 11, 2024 · fb19d33 · fb19d33
1 parent 0b35048
commit fb19d33
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 18 deletions.
diff --git 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
@@ -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
@@ -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
@@ -3,30 +3,30 @@
 (* 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 ->
         fun us ->
           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")
Original file line number	Diff line number	Diff line change
		@@ -1,3 +1,4 @@
		open FStar_All

		(* TODO: make this an F* module, no need to drop to OCaml for this *)

Expand Down