syntax change in FStar.Classical, for a binder that used a non-simple…

… function type
FStarLang · Feb 12, 2018 · 6bcaede · 6bcaede
1 parent 1f0210b
commit 6bcaede
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst
@@ -99,7 +99,7 @@ let exists_elim goal #a #p have f =
   bind_squash #_ #goal (join_squash have) (fun (| x, pf |) -> return_squash pf; f x)
 
 let move_requires (#a:Type) (#p:a -> Type) (#q:a -> Type)
-  ($f:x:a -> Lemma (requires (p x)) (ensures (q x))) (x:a)
+  ($f:(x:a -> Lemma (requires (p x)) (ensures (q x)))) (x:a)
   : Lemma (p x ==> q x) =
       give_proof
         (bind_squash (get_proof (l_or (p x) (~(p x))))