Disentangle tactic notation resolution from Pcoq.

Instead of relying on entry names as given by a hardwired registering
scheme in Pcoq, we recover them first through a user-defined map, and
fallback on generic argument names.

3 files changed, 31 insertions, 7 deletions

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index fbae17baf..0bddcc9fd 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -40,6 +40,16 @@ let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
   Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
 
+(** Backward-compatible tactic notation entry names *)
+
+let () =
+  let register name entry = Tacentries.register_tactic_notation_entry name entry in
+  register "hyp" wit_var;
+  register "simple_intropattern" wit_intro_pattern;
+  register "integer" wit_integer;
+  register "reference" wit_ref;
+  ()
+
 (* Rewriting orientation *)
 
 let _ = Metasyntax.add_token_obj "<-"
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index dfcfdece6..2adeb3a65 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -91,7 +91,6 @@ let rec parse_user_entry s sep =
     let n = Char.code s.[6] - 48 in
     Uentryl ("tactic", n)
   else
-    let s = match s with "hyp" -> "var" | _ -> s in
     Uentry s
 
 let arg_list = function Rawwit t -> Rawwit (ListArg t)
@@ -205,18 +204,30 @@ let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
 (**********************************************************************)
 (* Tactic Notation                                                    *)
 
+let entry_names = ref String.Map.empty
+
+let register_tactic_notation_entry name entry =
+  let entry = match entry with
+  | ExtraArg arg -> ArgT.Any arg
+  | _ -> assert false
+  in
+  entry_names := String.Map.add name entry !entry_names
+
 let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, (nt, sep), _) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
-      begin
-        try try_get_entry uprim s with Not_found ->
-        try try_get_entry uconstr s with Not_found ->
-        try try_get_entry utactic s with Not_found ->
-        error ("Unknown entry "^s^".")
-      end
+      let ArgT.Any arg =
+        if String.Map.mem s !entry_names then
+          String.Map.find s !entry_names
+        else match ArgT.name s with
+        | None -> error ("Unknown entry "^s^".")
+        | Some arg -> arg
+      in
+      let wit = ExtraArg arg in
+      EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
     | Some n ->
       (** FIXME: do better someday *)
       assert (String.equal s "tactic");
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index cd9f430cb..cdeb27ce6 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -20,6 +20,9 @@ val add_tactic_notation :
     environment at level [level] with locality [local] made of the grammar
     productions [prods] and returning the body [expr] *)
 
+val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit
+(** Register an argument under a given entry name for tactic notations. *)
+
 val add_ml_tactic_notation : ml_tactic_name ->
   Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list list -> unit