Merge PR #11740: Ltac2: Add notation for enough and eenough

Reviewed-by: ppedrot

3 files changed, 36 insertions, 0 deletions

diff --git a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
new file mode 100644
index 0000000000..ced3e0ab60
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 notations for enough an eenough
+  (`#11740 <https://github.com/coq/coq/pull/11740>`_,
+  by Michael Soegtrop).
diff --git a/test-suite/ltac2/example2.v b/test-suite/ltac2/example2.v
index c953d25061..ac92ca34ef 100644
--- a/test-suite/ltac2/example2.v
+++ b/test-suite/ltac2/example2.v
@@ -261,6 +261,25 @@ assert (H : 0 + 0 = 0) by reflexivity.
 intros x; exact x.
 Qed.
 
+Goal True.
+Proof.
+enough (H := 0 + 0).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+enough (exists n, n = 0) as [n Hn].
++ exact I.
++ exists 0; reflexivity.
+Qed.
+
+Goal True -> True.
+Proof.
+enough (H : 0 + 0 = 0) by (intros x; exact x).
+reflexivity.
+Qed.
+
 Goal 1 + 1 = 2.
 Proof.
 change (?a + 1 = 2) with (2 = $a + 1).
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index b650c1a2ec..d6bf4a28ba 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -265,6 +265,19 @@ Ltac2 Notation "assert" ast(thunk(assert)) := assert0 false ast.
 
 Ltac2 Notation "eassert" ast(thunk(assert)) := assert0 true ast.
 
+Ltac2 enough_from_assertion(a : Std.assertion) :=
+  match a with
+  | Std.AssertType ip_opt term tac_opt => Std.enough term (Some tac_opt) ip_opt
+  | Std.AssertValue ident constr => Std.pose (Some ident) constr
+  end.
+
+Ltac2 enough0 ev ast :=
+  enter_h ev (fun _ ast => enough_from_assertion ast) ast.
+
+Ltac2 Notation "enough" ast(thunk(assert)) := enough0 false ast.
+
+Ltac2 Notation "eenough" ast(thunk(assert)) := enough0 true ast.
+
 Ltac2 default_everywhere cl :=
 match cl with
 | None => { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }