Revert unnecessary changes to ulib.

ulib/FStar.Classical.fst

@@ -44,7 +44,7 @@ let arrow_to_impl #a #b f = squash_double_arrow (return_squash #(a -> GTot (squa
 
 let impl_intro_gtot #p #q f = return_squash f
 
-let impl_intro_tot #p #q f = return_squash #(p -> GTot q) fun x -> f x
+let impl_intro_tot #p #q f = return_squash #(p -> GTot q) f
 
 let impl_intro #p #q f =
   give_witness #(p ==> q) (squash_double_arrow (return_squash (lemma_to_squash_gtot f)))
@@ -92,13 +92,13 @@ let gtot_to_lemma #a #p f x = give_proof #(p x) (return_squash (f x))
 let forall_intro_squash_gtot #a #p f =
   bind_squash #(x: a -> GTot (p x))
     #(forall (x: a). p x)
-    (squash_double_arrow #a #(fun x -> p x) (return_squash f))
+    (squash_double_arrow #a #p (return_squash f))
     (fun f -> lemma_forall_intro_gtot #a #p f)
 
 let forall_intro_squash_gtot_join #a #p f =
   join_squash (bind_squash #(x: a -> GTot (p x))
         #(forall (x: a). p x)
-        (squash_double_arrow #a #(fun x -> p x) (return_squash f))
+        (squash_double_arrow #a #p (return_squash f))
         (fun f -> lemma_forall_intro_gtot #a #p f))
 
 let forall_intro #a #p f = give_witness (forall_intro_squash_gtot (lemma_to_squash_gtot #a #p f))
@@ -118,7 +118,7 @@ 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 (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 f
+let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #p 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) =
@@ -165,7 +165,7 @@ let exists_intro_not_all_not (#a:Type) (#p:a -> Type)
            (get_proof (forall x. ~ (p x)))
            (fun (g: (forall x. ~ (p x))) ->
              bind_squash #(x:a -> GTot (~(p x))) #Prims.empty g
-             (fun (h:(x:a -> GTot (~(p x)))) -> f fun x -> h x))
+             (fun (h:(x:a -> GTot (~(p x)))) -> f h))
     in
     ()
 #pop-options

ulib/FStar.Tactics.V1.Derived.fst

@@ -428,7 +428,7 @@ val (<|>) : (unit -> Tac 'a) ->
 let (<|>) t1 t2 = fun () -> or_else t1 t2
 
 let first (ts : list (unit -> Tac 'a)) : Tac 'a =
-    L.fold_right (fun t1 t2 () -> or_else t1 t2) ts (fun () -> fail "no tactics to try") ()
+    L.fold_right (<|>) ts (fun () -> fail "no tactics to try") ()
 
 let rec repeat (#a:Type) (t : unit -> Tac a) : Tac (list a) =
     match catch t with

ulib/FStar.Tactics.V2.Derived.fst

@@ -482,7 +482,7 @@ val (<|>) : (unit -> Tac 'a) ->
 let (<|>) t1 t2 = fun () -> or_else t1 t2
 
 let first (ts : list (unit -> Tac 'a)) : Tac 'a =
-    L.fold_right (fun t1 t2 () -> or_else t1 t2) ts (fun () -> fail "no tactics to try") ()
+    L.fold_right (<|>) ts (fun () -> fail "no tactics to try") ()
 
 let rec repeat (#a:Type) (t : unit -> Tac a) : Tac (list a) =
     match catch t with

ulib/LowStar.RVector.fst

@@ -74,7 +74,7 @@ val rs_elems_inv:
   i:nat -> j:nat{i <= j && j <= S.length rs} ->
   GTot Type0
 let rs_elems_inv #a #rst rg h rs i j =
-  V.forall_seq rs i j (fun x -> rg_inv rg h x)
+  V.forall_seq rs i j (rg_inv rg h)
 
 val rv_elems_inv:
   #a:Type0 -> #rst:Type -> #rg:regional rst a ->

ulib/legacy/FStar.Buffer.Quantifiers.fst

@@ -35,7 +35,7 @@ let lemma_sub_quantifiers #a h b b' i len =
   let lemma_post (j:nat) = j < length b' ==> get h b' j == get h b (j + v i) in
   let qj : j:nat -> Lemma (lemma_post j)
     = fun j -> assert (j < v len ==> Seq.index (as_seq h b') j == Seq.index (as_seq h b) (j + v i)) in
-  Classical.forall_intro #_ #(fun x -> lemma_post x) qj
+  Classical.forall_intro #_ #lemma_post qj
 
 val lemma_offset_quantifiers: #a:Type -> h:mem -> b:buffer a -> b':buffer a -> i:FStar.UInt32.t{v i <= length b} -> Lemma
   (requires (live h b /\ live h b' /\ Seq.slice (as_seq h b) (v i) (length b) == as_seq h b'))
@@ -56,7 +56,7 @@ let lemma_create_quantifiers #a h b init len =
   let lemma_post (i:nat) = i < length b ==> get h b i == init in
   let qi : i:nat -> Lemma (lemma_post i) = 
    fun i -> assert (i < length b ==> get h b i == Seq.index (as_seq h b) i) in
-  Classical.forall_intro #_ #(fun x -> lemma_post x) qi
+  Classical.forall_intro #_ #lemma_post qi
 
 val lemma_index_quantifiers: #a:Type -> h:mem -> b:buffer a -> n:FStar.UInt32.t -> Lemma
   (requires (live h b /\ v n < length b))
@@ -101,8 +101,8 @@ let lemma_blit_quantifiers #a h0 h1 b bi b' bi' len =
 	  ==> Seq.index (Seq.slice (as_seq h1 b') (v bi'+v len) (length b')) (j - (v bi'+v len))
 	      == Seq.index (Seq.slice (as_seq h0 b') (v bi'+v len) (length b')) (j - (v bi'+v len)))
 	in
-  Classical.forall_intro #_ #(fun x -> lemma_post_1 x) qj_1;
-  Classical.forall_intro #_ #(fun x -> lemma_post_2 x) qj_2
+  Classical.forall_intro #_ #lemma_post_1 qj_1;
+  Classical.forall_intro #_ #lemma_post_2 qj_2
 
 
 (* Equality predicate between buffers with quantifiers *)
@@ -116,4 +116,4 @@ let eq_lemma #a h b h' b' =
   let lemma_post (j:nat) = j < length b ==> get h b j == get h' b' j in
   let qj : j:nat -> Lemma (lemma_post j) = fun j ->
     assert(j < length b ==> Seq.index (as_seq h b) j == Seq.index (as_seq h' b') j) in
-  Classical.forall_intro #_ #(fun x -> lemma_post x) qj
+  Classical.forall_intro #_ #lemma_post qj