Merge pull request #3924 from mtzguido/tactics

Tactics: make V2 the default

Author: mtzguido

tests/micro-benchmarks/Misc.Norm3.fst

@@ -8,6 +8,7 @@ will fail to typecheck. *)
 open FStar.Ghost
 open FStar.Tactics
 open FStar.Reflection.Typing
+module R = FStar.Reflection
 
 [@@erasable]
 noeq
@@ -16,21 +17,21 @@ type my_erased (a:Type) = | E of a
 let test (r_env goal : _) : Tac unit =
   let u0 = pack_universe Uv_Zero in
   let goal_typing :
-    my_erased (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0)))
+    my_erased (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0)))
     = magic()
   in
-  let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0))) =
+  let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0))) =
     match goal_typing with E x -> ()
   in
   ()
 
 (* This should always work regardless of the comment above. *)
 let test2 (r_env goal u0 : _) : Tac unit =
   let goal_typing :
-    my_erased (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0)))
+    my_erased (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0)))
     = magic()
   in
-  let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0))) =
+  let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0))) =
     match goal_typing with E x -> ()
   in
   ()

tests/tactics/NoDuplicateSplice.fst

@@ -3,11 +3,11 @@ module NoDuplicateSplice
 open FStar.Tactics
 
 let mk (nm:string) (i:int) : Tac decls =
-  let lb = pack_lb ({ lb_fv = pack_fv (cur_module() @ [nm])
-                    ; lb_us = []
-                    ; lb_typ = `int
-                    ; lb_def = pack (Tv_Const (C_Int i)) }) in
-  [pack_sigelt (Sg_Let false [lb])]
+  let lb = { lb_fv = pack_fv (cur_module() @ [nm])
+           ; lb_us = []
+           ; lb_typ = `int
+           ; lb_def = pack (Tv_Const (C_Int i)) } in
+  [pack_sigelt (Sg_Let {isrec=false; lbs=[lb]})]
 
 %splice[] (mk "x" 1)
 

ulib/FStar.Reflection.Formula.fst

@@ -16,4 +16,4 @@
 module FStar.Reflection.Formula
 
 (* This module is a temporary for Meta-F* migration *)
-include FStar.Reflection.V1.Formula
+include FStar.Reflection.V2.Formula

ulib/FStar.Reflection.fst

@@ -15,6 +15,6 @@
 *)
 module FStar.Reflection
 
-(* This switch currently points to V1. Ask for V2 explicitly by
-importing FStar.Reflection.V2 *)
-include FStar.Reflection.V1
+(* This switch currently points to V2. Ask for V1 explicitly by
+importing FStar.Reflection.V1 *)
+include FStar.Reflection.V2

ulib/FStar.Tactics.Builtins.fsti

@@ -16,4 +16,4 @@
 module FStar.Tactics.Builtins
 
 (* This module is a temporary for Meta-F* migration *)
-include FStar.Stubs.Tactics.V1.Builtins
+include FStar.Stubs.Tactics.V2.Builtins

ulib/FStar.Tactics.Derived.fst

@@ -16,4 +16,4 @@
 module FStar.Tactics.Derived
 
 (* This module is a temporary for Meta-F* migration *)
-include FStar.Tactics.V1.Derived
+include FStar.Tactics.V2.Derived

ulib/FStar.Tactics.Logic.fst

@@ -16,4 +16,4 @@
 module FStar.Tactics.Logic
 
 (* This module is a temporary for Meta-F* migration *)
-include FStar.Tactics.V1.Logic
+include FStar.Tactics.V2.Logic

ulib/FStar.Tactics.SyntaxHelpers.fst

@@ -16,4 +16,4 @@
 module FStar.Tactics.SyntaxHelpers
 
 (* This module is a temporary for Meta-F* migration *)
-include FStar.Tactics.V1.SyntaxHelpers
+include FStar.Tactics.V2.SyntaxHelpers

ulib/FStar.Tactics.V2.Logic.fsti

@@ -21,7 +21,7 @@ open FStar.Reflection.V2.Formula
 open FStar.Tactics.NamedView
 open FStar.Tactics.Logic.Lemmas {} (* bring lemmas into TC scope *)
 
-(* Repeated to avoid importing FStar.Tactics.V1.Derived. *)
+(* Repeated to avoid importing FStar.Tactics.Derived. *)
 private let cur_goal () : Tac typ =
   let open FStar.Stubs.Tactics.Types in
   let open FStar.Stubs.Tactics.V2.Builtins in

ulib/FStar.Tactics.fsti

@@ -15,4 +15,4 @@
 *)
 module FStar.Tactics
 
-include FStar.Tactics.V1
+include FStar.Tactics.V2