Adding quotations for the generalize tactic.

1 files changed, 6 insertions, 0 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index 9b39942ca5..e393002f55 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -284,6 +284,12 @@ Ltac2 Notation "einduction"
   use(thunk(opt(seq("using", constr, with_bindings)))) :=
   induction0 true ic use.
 
+Ltac2 generalize0 gen :=
+  enter_h false (fun _ gen => Std.generalize gen) gen.
+
+Ltac2 Notation "generalize" gen(thunk(generalizations)) :=
+  generalize0 gen.
+
 Ltac2 destruct0 ev ic use :=
   let f ev use := Std.destruct ev ic use in
   enter_h ev f use.