Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Require`.

3 files changed, 18 insertions, 0 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 4e62fab715..bfd2ab1a11 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -650,6 +650,7 @@ END
 
 (** Extension of constr syntax *)
 
+let () = Hook.set Tac2entries.register_constr_quotations begin fun () ->
 GEXTEND Gram
   Pcoq.Constr.operconstr: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
@@ -666,6 +667,7 @@ GEXTEND Gram
     ] ]
   ;
 END
+end
 
 let pr_ltac2entry _ = mt () (** FIXME *)
 let pr_ltac2expr _ = mt () (** FIXME *)
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index da7c07c134..2895fda060 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -819,10 +819,22 @@ let def_unit = {
 
 let t_list = coq_def "list"
 
+let (f_register_constr_quotations, register_constr_quotations) = Hook.make ()
+
+let perform_constr_quotations (_, ()) = Hook.get f_register_constr_quotations ()
+
+(** Dummy object that register global rules when Require is called *)
+let inTac2ConstrQuotations : unit -> obj =
+  declare_object {(default_object "TAC2-CONSTR-QUOT") with
+    cache_function = perform_constr_quotations;
+    load_function = fun _ -> perform_constr_quotations;
+  }
+
 let _ = Mltop.declare_cache_obj begin fun () ->
   ignore (Lib.add_leaf (Id.of_string "unit") (inTypDef def_unit));
   register_prim_alg "list" 1 [
     ("[]", []);
     ("::", [GTypVar 0; GTypRef (Other t_list, [GTypVar 0])]);
   ];
+  Lib.add_anonymous_leaf (inTac2ConstrQuotations ());
 end "ltac2_plugin"
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index acb99a34b1..7ed45e62e5 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -72,3 +72,7 @@ val q_occurrences : occurrences Pcoq.Gram.entry
 val q_reference : Libnames.reference or_anti Pcoq.Gram.entry
 val q_strategy_flag : strategy_flag Pcoq.Gram.entry
 end
+
+(** {5 Hooks} *)
+
+val register_constr_quotations : (unit -> unit) Hook.t