From 46095430ed07306ba3380ea8192540793c5c0a26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Sep 2017 21:44:43 +0200
Subject: Adding quotations for the generalize tactic.

---
 theories/Notations.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'theories')

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.
-- 
cgit v1.2.3