Update tests

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)