Adding more notations for the lulz.

2 files changed, 33 insertions, 4 deletions

diff --git a/tests/example2.v b/tests/example2.v
index 95485305dc..a7eb02050b 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -192,3 +192,19 @@ unfold &x at 1.
 let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
 reflexivity.
 Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+exists 0, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+eexists _, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+refine '(let x := 0 in _).
+eexists; exists &x; reflexivity.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 8345344d94..2a496b3faf 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -140,12 +140,11 @@ Ltac2 exists0 ev bnds := match bnds with
   aux bnds
 end.
 
-(*
-Ltac2 Notation "exists" bnd(list0(thunk(with_bindings), ",")) := exists0 false bnd.
+Ltac2 Notation "exists" bnd(list0(thunk(bindings), ",")) := exists0 false bnd.
+(* Ltac2 Notation exists := exists. *)
 
-Ltac2 Notation "eexists" bnd(list0(thunk(with_bindings), ",")) := exists0 true bnd.
+Ltac2 Notation "eexists" bnd(list0(thunk(bindings), ",")) := exists0 true bnd.
 Ltac2 Notation eexists := eexists.
-*)
 
 Ltac2 left0 ev bnd := enter_h ev Std.left bnd.
 
@@ -308,6 +307,20 @@ Ltac2 Notation "erewrite"
 
 (** coretactics *)
 
+Ltac2 exact0 ev c :=
+  Control.enter (fun _ =>
+    match ev with
+    | true =>
+      let c := c () in
+      Control.refine (fun _ => c)
+    | false =>
+      Control.with_holes c (fun c => Control.refine (fun _ => c))
+    end
+  ).
+
+Ltac2 Notation "exact" c(thunk(open_constr)) := exact0 false c.
+Ltac2 Notation "eexact" c(thunk(open_constr)) := exact0 true c.
+
 Ltac2 Notation reflexivity := Std.reflexivity ().
 
 Ltac2 Notation assumption := Std.assumption ().