Revert unnecessary changes to ulib.

ulib/FStar.Classical.fst

@@ -115,10 +115,10 @@ let forall_intro_2 #a #b #p f =
 let forall_intro_2_with_pat #a #b #c #p pat f = forall_intro_2 #a #b #p f
 
 let forall_intro_3 #a #b #c #p f =
-  let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 #_ #_ #(fun y z -> p x y z) (f x) in
+  let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 (f x) in
   forall_intro g
 
-let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #(fun x y z -> p x y z) f
+let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c f
 
 let forall_intro_4 #a #b #c #d #p f =
   let g: x: a -> Lemma (forall (y: b x) (z: c x y) (w: d x y z). p x y z w) =

ulib/FStar.Classical.fsti

@@ -321,7 +321,7 @@ val forall_intro_4
     TODO: Seems overly specific; could be removed?  *)
 val forall_impl_intro
       (#a: Type)
-      (#p #q: (a -> Type))
+      (#p #q: (a -> GTot Type))
       ($_: (x: a -> squash (p x) -> Lemma (q x)))
     : Lemma (forall x. p x ==> q x)
 
@@ -331,7 +331,7 @@ val forall_impl_intro
   *)
 val ghost_lemma
       (#a: Type)
-      (#p: (a -> Type0))
+      (#p: (a -> GTot Type0))
       (#q: (a -> unit -> GTot Type0))
       ($_: (x: a -> Lemma (requires p x) (ensures (q x ()))))
     : Lemma (forall (x: a). p x ==> q x ())

ulib/FStar.Modifies.fst

@@ -95,7 +95,7 @@ let loc_aux_includes_trans'
   (s3: loc_aux)
 : Lemma
   ((loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3) ==> loc_aux_includes s1 s3)
-= Classical.move_requires #_ #_ #(fun s3 -> loc_aux_includes s1 s3) (loc_aux_includes_trans s1 s2) s3
+= Classical.move_requires (loc_aux_includes_trans s1 s2) s3
 
 let loc_aux_disjoint_buffer
   (l: loc_aux)

ulib/FStar.ModifiesGen.fst

@@ -352,7 +352,7 @@ let loc_aux_includes_buffer_includes
 : Lemma
   (requires (loc_aux_includes_buffer s b1 /\ b1 `aloc_includes` b2))
   (ensures (loc_aux_includes_buffer s b2))
-= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires #_ #_ #(fun x3 -> c.aloc_includes b1 x3) (c.aloc_includes_trans #r #a b1 b2) b3))
+= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3))
 
 let loc_aux_includes_loc_aux_includes_buffer
   (#al: aloc_t) (#c: cls al)
@@ -361,15 +361,15 @@ let loc_aux_includes_loc_aux_includes_buffer
 : Lemma
   (requires (loc_aux_includes s1 s2 /\ loc_aux_includes_buffer s2 b))
   (ensures (loc_aux_includes_buffer s1 b))
-= Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires #_ #_ #(fun b2 -> loc_aux_includes_buffer s b2) (loc_aux_includes_buffer_includes #al #c s b1) b2)
+= Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires (loc_aux_includes_buffer_includes #al #c s b1) b2)
 
 let loc_aux_includes_trans
   (#al: aloc_t) (#c: cls al)
   (s1 s2 s3: GSet.set (aloc c))
 : Lemma
   (requires (loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3))
   (ensures (loc_aux_includes s1 s3))
-= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires #_ #_ #(fun x3 -> c.aloc_includes b1 x3) (c.aloc_includes_trans #r #a b1 b2) b3))
+= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3))
 
 let addrs_of_loc_weak_loc_union
   (#al: aloc_t) (#c: cls al)
@@ -590,7 +590,7 @@ let loc_aux_disjoint_loc_aux_includes
   (ensures (loc_aux_disjoint l1 l3))
 = // FIXME: WHY WHY WHY do I need this assert?
   assert (forall (b1 b3: aloc c) . (GSet.mem b1 l1 /\ GSet.mem b3 l3) ==> (exists (b2: aloc c) . GSet.mem b2 l2 /\ aloc_disjoint b1 b2 /\ aloc_includes b2 b3));
-  Classical.forall_intro_3 (fun b1 b2 b3 -> Classical.move_requires #_ #_ #(fun b3 -> aloc_disjoint b1 b3) (aloc_disjoint_includes #al #c b1 b2) b3)
+  Classical.forall_intro_3 (fun b1 b2 b3 -> Classical.move_requires (aloc_disjoint_includes #al #c b1 b2) b3)
 
 let loc_disjoint_includes #al #c p1 p2 p1' p2' =
   regions_of_loc_monotonic p1 p1';
@@ -1028,7 +1028,7 @@ let modifies_refl #al #c s h =
 let modifies_loc_includes #al #c s1 h h' s2 =
   assert (modifies_preserves_mreferences s1 h h');
   Classical.forall_intro_2 (loc_aux_disjoint_sym #al #c);
-  Classical.forall_intro_3 (fun l1 l2 l3 -> Classical.move_requires #_ #_ #(fun l3 -> loc_aux_disjoint l1 l3) (loc_aux_disjoint_loc_aux_includes #al #c l1 l2) l3);
+  Classical.forall_intro_3 (fun l1 l2 l3 -> Classical.move_requires (loc_aux_disjoint_loc_aux_includes #al #c l1 l2) l3);
   assert (modifies_preserves_alocs s1 h h')
 
 let modifies_preserves_liveness #al #c s1 s2 h h' #t #pre r = ()
@@ -1078,7 +1078,7 @@ let modifies_trans'
 : Lemma
   (requires (modifies s h1 h2 /\ modifies s h2 h3))
   (ensures (modifies s h1 h3))
-= Classical.forall_intro_3 (fun r a b -> Classical.move_requires #_ #_ #(fun h3 -> c.aloc_preserved b h1 h3) (c.aloc_preserved_trans #r #a b h1 h2) h3)
+= Classical.forall_intro_3 (fun r a b -> Classical.move_requires (c.aloc_preserved_trans #r #a b h1 h2) h3)
 
 let modifies_trans #al #c s12 h1 h2 s23 h3 =
   let u = loc_union s12 s23 in
@@ -1112,7 +1112,7 @@ let modifies_only_live_regions_weak
   ))
   (ensures (modifies l h h'))
 = assert (modifies_preserves_mreferences l h h'); // FIXME: WHY WHY WHY?
-  Classical.forall_intro_3 (fun r a b -> Classical.move_requires #_ #_ #(fun h2 -> c.aloc_preserved b h h2) (addr_unused_in_aloc_preserved #al #c #r #a b h) h')
+  Classical.forall_intro_3 (fun r a b -> Classical.move_requires (addr_unused_in_aloc_preserved #al #c #r #a b h) h')
 #pop-options
 
 (* Restrict a set of locations along a set of regions *)
@@ -1545,7 +1545,7 @@ let modifies_only_not_unused_in #al #c l h h' =
 
 #push-options "--z3rlimit 20"
 let mreference_live_loc_not_unused_in #al c #t #pre h b =
-  Classical.move_requires #_ #(fun ra -> does_not_contain_addr h ra) (does_not_contain_addr_addr_unused_in h) (HS.frameOf b, HS.as_addr b);
+  Classical.move_requires (does_not_contain_addr_addr_unused_in h) (HS.frameOf b, HS.as_addr b);
   assert (~ (h `does_not_contain_addr` (HS.frameOf b, HS.as_addr b)));
   loc_addresses_not_unused_in c (HS.frameOf b) (Set.singleton (HS.as_addr b)) h;
   loc_includes_trans (loc_not_unused_in c h) (loc_freed_mreference b) (loc_mreference b);
@@ -1554,7 +1554,7 @@ let mreference_live_loc_not_unused_in #al c #t #pre h b =
 
 #push-options "--z3cliopt 'smt.qi.eager_threshold=100'"
 let mreference_unused_in_loc_unused_in #al c #t #pre h b =
-  Classical.move_requires #_ #_ #(fun ra -> does_not_contain_addr h ra) (addr_unused_in_does_not_contain_addr h) (HS.frameOf b, HS.as_addr b);
+  Classical.move_requires (addr_unused_in_does_not_contain_addr h) (HS.frameOf b, HS.as_addr b);
   loc_addresses_unused_in c (HS.frameOf b) (Set.singleton (HS.as_addr b)) h;
   loc_includes_addresses_addresses c false true (HS.frameOf b) (Set.singleton (HS.as_addr b)) (Set.singleton (HS.as_addr b));
   loc_includes_trans (loc_unused_in c h) (loc_freed_mreference b) (loc_mreference b);
@@ -1874,7 +1874,7 @@ let union_loc_of_loc_includes_elim
     (x: aloc (c b))
   : Lemma
     ((GSet.mem x auxs /\ (~ (GSet.mem x.addr (addrs_of_loc_weak smaller x.region)))) ==> g' r a x)
-  = Classical.move_requires #_ #_ #(fun x-> g' r a x) (f r a) x
+  = Classical.move_requires (f r a) x
   in
   Classical.forall_intro_3 f';
   assert (forall (r: HS.rid) (a: nat) (x: aloc (c b)) .
@@ -1896,8 +1896,8 @@ let union_loc_of_loc_includes_elim
 #pop-options
 
 let union_loc_of_loc_includes #al c b s1 s2 =
-  Classical.move_requires #_ #_ #(fun s2 -> loc_includes s1 s2) (union_loc_of_loc_includes_elim c b s1) s2;
-  Classical.move_requires #_ #(fun s2 -> loc_includes s1 s2) (union_loc_of_loc_includes_intro c b s1) s2
+  Classical.move_requires (union_loc_of_loc_includes_elim c b s1) s2;
+  Classical.move_requires (union_loc_of_loc_includes_intro c b s1) s2
 
 #push-options "--fuel 0 --ifuel 0"
 let union_loc_of_loc_disjoint_intro
@@ -1979,8 +1979,8 @@ let union_loc_of_loc_disjoint_elim
 #pop-options
 
 let union_loc_of_loc_disjoint #al c b s1 s2 =
-  Classical.move_requires #_ #_ #(fun s2 -> loc_disjoint s1 s2) (union_loc_of_loc_disjoint_elim c b s1) s2;
-  Classical.move_requires #_ #(fun s2 -> loc_disjoint s1 s2) (union_loc_of_loc_disjoint_intro c b s1) s2
+  Classical.move_requires (union_loc_of_loc_disjoint_elim c b s1) s2;
+  Classical.move_requires (union_loc_of_loc_disjoint_intro c b s1) s2
 
 #push-options "--z3rlimit 32"
 let modifies_union_loc_of_loc_elim
@@ -2067,8 +2067,8 @@ let modifies_union_loc_of_loc_intro
 #pop-options
 
 let modifies_union_loc_of_loc #al c b l h1 h2 =
-  Classical.move_requires #_ #(fun h2 -> modifies (union_loc_of_loc c b l) h1 h2) #(fun h2 -> modifies l h1 h2) (modifies_union_loc_of_loc_elim c b l h1) h2;
-  Classical.move_requires #_ #(fun h2 -> modifies l h1 h2) #(fun h2 -> modifies (union_loc_of_loc c b l) h1 h2) (modifies_union_loc_of_loc_intro c b l h1) h2
+  Classical.move_requires (modifies_union_loc_of_loc_elim c b l h1) h2;
+  Classical.move_requires (modifies_union_loc_of_loc_intro c b l h1) h2
 
 let loc_of_union_loc #al #c b l
 = let (Loc regions region_liveness_tags non_live_addrs live_addrs aux) = l in

ulib/FStar.Tactics.V1.Logic.Lemmas.fst

@@ -16,7 +16,7 @@
 module FStar.Tactics.V1.Logic.Lemmas
 
 let fa_intro_lem (#a:Type) (#p:a -> Type) (f:(x:a -> squash (p x))) : Lemma (forall (x:a). p x) =
-  FStar.Classical.lemma_forall_intro_gtot #_ #(fun x -> p x)
+  FStar.Classical.lemma_forall_intro_gtot
     ((fun x -> FStar.IndefiniteDescription.elim_squash (f x)) <: (x:a -> GTot (p x)))
 
 let split_lem #a #b sa sb = ()

ulib/LowStar.Monotonic.Buffer.fst

@@ -383,7 +383,7 @@ let ubuffer_preserved_intro
     ) ==>
     Seq.equal (Seq.slice (as_seq h b') (boff - U32.v idx) (boff - U32.v idx + blen)) (Seq.slice (as_seq h' b') (boff - U32.v idx) (boff - U32.v idx + blen))
   )))))
-  = Classical.move_requires #_ #_ #(fun b' -> live h' b') (f0 t' rrel rel) b';
+  = Classical.move_requires (f0 t' rrel rel) b';
     Classical.move_requires (f t' rrel rel) b'
   in
   Classical.forall_intro_4 g'
@@ -899,10 +899,10 @@ let loc_includes_union_r'
   (loc_includes s (loc_union s1 s2) <==> (loc_includes s s1 /\ loc_includes s s2))
   [SMTPat (loc_includes s (loc_union s1 s2))]
 = Classical.move_requires (loc_includes_union_r s s1) s2;
-  Classical.move_requires #_ #_ #(fun s -> loc_includes (loc_union s1 s2) s) (loc_includes_union_l s1 s2) s1;
-  Classical.move_requires #_ #_ #(fun s -> loc_includes (loc_union s1 s2) s) (loc_includes_union_l s1 s2) s2;
-  Classical.move_requires #_ #_ #(fun s3 -> loc_includes s s3) (loc_includes_trans s (loc_union s1 s2)) s1;
-  Classical.move_requires #_ #_ #(fun s3 -> loc_includes s s3) (loc_includes_trans s (loc_union s1 s2)) s2
+  Classical.move_requires (loc_includes_union_l s1 s2) s1;
+  Classical.move_requires (loc_includes_union_l s1 s2) s2;
+  Classical.move_requires (loc_includes_trans s (loc_union s1 s2)) s1;
+  Classical.move_requires (loc_includes_trans s (loc_union s1 s2)) s2
 
 let loc_includes_none = MG.loc_includes_none
 
@@ -1456,13 +1456,13 @@ let fresh_frame_loc_not_unused_in_disjoint
 
 let live_loc_not_unused_in #_ #_ #_ b h =
   unused_in_equiv b h;
-  Classical.move_requires #_ #(fun ra -> MG.does_not_contain_addr h ra) (MG.does_not_contain_addr_addr_unused_in h) (frameOf b, as_addr b);
+  Classical.move_requires (MG.does_not_contain_addr_addr_unused_in h) (frameOf b, as_addr b);
   MG.loc_addresses_not_unused_in cls (frameOf b) (Set.singleton (as_addr b)) h;
   ()
 
 let unused_in_loc_unused_in #_ #_ #_ b h =
   unused_in_equiv b h;
-  Classical.move_requires #_ #_ #(fun ra -> MG.does_not_contain_addr h ra) (MG.addr_unused_in_does_not_contain_addr h) (frameOf b, as_addr b);
+  Classical.move_requires (MG.addr_unused_in_does_not_contain_addr h) (frameOf b, as_addr b);
   MG.loc_addresses_unused_in cls (frameOf b) (Set.singleton (as_addr b)) h;
   ()
 

ulib/legacy/FStar.Pointer.Base.fst

@@ -3214,8 +3214,8 @@ let disjoint_sym'
   (requires True)
   (ensures (disjoint p1 p2 <==> disjoint p2 p1))
   [SMTPat (disjoint p1 p2)]
-= FStar.Classical.move_requires #_ #(fun p2 -> disjoint p1 p2) (disjoint_sym #value1 #value2 p1) p2;
-  FStar.Classical.move_requires #_ #(fun p1 -> disjoint p2 p1) (disjoint_sym #value2 #value1 p2) p1
+= FStar.Classical.move_requires (disjoint_sym #value1 #value2 p1) p2;
+  FStar.Classical.move_requires (disjoint_sym #value2 #value1 p2) p1
 
 let disjoint_sym''
   (value1: typ)
@@ -3407,7 +3407,7 @@ let loc_aux_includes_trans'
   (s3: loc_aux)
 : Lemma
   ((loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3) ==> loc_aux_includes s1 s3)
-= Classical.move_requires #_ #_ #(fun s3 -> loc_aux_includes s1 s3) (loc_aux_includes_trans s1 s2) s3
+= Classical.move_requires (loc_aux_includes_trans s1 s2) s3
 
 
 (* Disjointness of two memory locations *)
@@ -3605,7 +3605,7 @@ let disjoint_not_self
   (p: pointer t)
 : Lemma
   (disjoint p p ==> False)
-= Classical.move_requires #_ #(fun p2 -> path_disjoint (Pointer?.p p) p2) (path_disjoint_not_path_equal (Pointer?.p p)) (Pointer?.p p)
+= Classical.move_requires (path_disjoint_not_path_equal (Pointer?.p p)) (Pointer?.p p)
 
 let loc_aux_in_addr
   (l: loc_aux)