Adding quotations for the generalize tactic.

8 files changed, 43 insertions, 1 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 7295f31181..dad1b71685 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -369,7 +369,7 @@ GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
           q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
           q_destruction_arg q_reference q_with_bindings q_constr_matching
-          q_hintdb q_move_location;
+          q_hintdb q_move_location q_generalizations;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -702,6 +702,22 @@ GEXTEND Gram
   q_move_location:
     [ [ mv = move_location -> mv ] ]
   ;
+  opt_generalization:
+    [ [ occs = occs; na = OPT ident_or_anti -> (occs, na)
+      | -> Loc.tag ~loc:!@loc QAllOccurrences, None
+    ] ]
+  ;
+  generalization:
+    [ [ c = Constr.constr; (occs, na) = opt_generalization ->
+        Loc.tag ~loc:!@loc (c, occs, na)
+    ] ]
+  ;
+  generalizations:
+    [ [ g = LIST1 generalization SEP "," -> Loc.tag ~loc:!@loc g ] ]
+  ;
+  q_generalizations:
+    [ [ g = generalizations -> g ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7bd0164b4d..1eef098311 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1118,6 +1118,7 @@ let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
 let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
 let () = add_expr_scope "reference" q_reference Tac2quote.of_reference
 let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_location
+let () = add_expr_scope "generalizations" q_generalizations Tac2quote.of_generalizations
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 26f96f7d72..2025753aec 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -40,6 +40,7 @@ let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
 let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
 let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
 let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
+let q_generalizations = Pcoq.Gram.entry_create "tactic:q_generalizations"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 7c71130402..d91032c2a8 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -79,6 +79,7 @@ val q_strategy_flag : strategy_flag Pcoq.Gram.entry
 val q_constr_matching : constr_matching Pcoq.Gram.entry
 val q_hintdb : hintdb Pcoq.Gram.entry
 val q_move_location : move_location Pcoq.Gram.entry
+val q_generalizations : generalizations Pcoq.Gram.entry
 end
 
 (** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 7d02022e07..59c7ad6f3f 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -139,3 +139,8 @@ type move_location_r =
 | QMoveLast
 
 type move_location = move_location_r located
+
+type generalization =
+  (Constrexpr.constr_expr * occurrences * Id.t located or_anti option) located
+
+type generalizations = generalization list located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index f14612d58f..a5c5c7d31f 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -370,3 +370,13 @@ let of_move_location (loc, mv) = match mv with
 | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
 | QMoveFirst -> std_constructor ?loc "MoveFirst" []
 | QMoveLast -> std_constructor ?loc "MoveLast" []
+
+let of_generalization (loc, (c, occ, na)) =
+  of_tuple ?loc [
+    of_open_constr c;
+    of_occurrences occ;
+    of_option (fun id -> of_anti of_ident id) na;
+  ]
+
+let of_generalizations (loc, l) =
+  of_list ?loc of_generalization l
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 9f42c60042..d31ce455eb 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -71,6 +71,8 @@ val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 val of_exact_var : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 (** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
 
+val of_generalizations : generalizations -> raw_tacexpr
+
 val of_dispatch : dispatch -> raw_tacexpr
 
 val of_strategy_flag : strategy_flag -> raw_tacexpr
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.