Use a simpler syntax for generalize grammar.

This removes the use for a quotation.

7 files changed, 1 insertions, 37 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index dad1b71685..7295f31181 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_generalizations;
+          q_hintdb q_move_location;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -702,22 +702,6 @@ 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 1eef098311..7bd0164b4d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1118,7 +1118,6 @@ 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 2025753aec..26f96f7d72 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -40,7 +40,6 @@ 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 d91032c2a8..7c71130402 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -79,7 +79,6 @@ 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 59c7ad6f3f..7d02022e07 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -139,8 +139,3 @@ 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 a5c5c7d31f..f14612d58f 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -370,13 +370,3 @@ 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 d31ce455eb..9f42c60042 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -71,8 +71,6 @@ 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