Adding a notation scope for global references.

6 files changed, 18 insertions, 7 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index ef3615db89..4a7ba31373 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -317,7 +317,8 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 
 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_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
+          q_reference;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -584,6 +585,9 @@ GEXTEND Gram
       | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
     ] ]
   ;
+  q_reference:
+    [ [ r = refglobal -> r ] ]
+  ;
   refglobals:
     [ [ gl = LIST1 refglobal -> Loc.tag ~loc:!@loc gl ] ]
   ;
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b38f0b8582..6c38d1dfd5 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -933,6 +933,7 @@ let () = add_expr_scope "clause" q_clause Tac2quote.of_clause
 let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences
 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_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index a6c0e21ac5..d2b69aaf7d 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -33,6 +33,7 @@ let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
 let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
 let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
 let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences"
+let q_reference = Pcoq.Gram.entry_create "tactic:q_reference"
 let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
 end
 
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 645d37a8c6..8b92bd16f6 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -68,5 +68,6 @@ val q_rewriting : rewriting Pcoq.Gram.entry
 val q_clause : clause Pcoq.Gram.entry
 val q_dispatch : dispatch Pcoq.Gram.entry
 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
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 4fcbcb5424..9778bd18ae 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -268,15 +268,17 @@ let make_red_flag l =
      rZeta = false; rDelta = false; rConst = []}
     l
 
+let of_reference r =
+  let of_ref ref =
+    let loc = Libnames.loc_of_reference ref in
+    inj_wit ?loc Tac2env.wit_reference ref
+  in
+  of_anti of_ref r
+
 let of_strategy_flag (loc, flag) =
   let open Genredexpr in
   let loc = Option.default dummy_loc loc in
   let flag = make_red_flag flag in
-  let of_reference ref =
-    let loc = Libnames.loc_of_reference ref in
-    inj_wit ?loc Tac2env.wit_reference ref
-  in
-  let of_ref r = of_anti of_reference r in
   CTacRec (loc, [
     std_proj "rBeta", of_bool ~loc flag.rBeta;
     std_proj "rMatch", of_bool ~loc flag.rMatch;
@@ -284,5 +286,5 @@ let of_strategy_flag (loc, flag) =
     std_proj "rCofix", of_bool ~loc flag.rCofix;
     std_proj "rZeta", of_bool ~loc flag.rZeta;
     std_proj "rDelta", of_bool ~loc flag.rDelta;
-    std_proj "rConst", of_list ~loc of_ref flag.rConst;
+    std_proj "rConst", of_list ~loc of_reference flag.rConst;
   ])
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 730324d051..bd2303ac98 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -48,6 +48,8 @@ val of_rewriting : rewriting -> raw_tacexpr
 
 val of_occurrences : occurrences -> raw_tacexpr
 
+val of_reference : Libnames.reference or_anti -> raw_tacexpr
+
 val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 (** id ↦ 'Control.hyp @id' *)