Stronger disambiguation of vernac extension names.

We prepend the plugin name to the vernac entry name. This prevents accidental
conflict between two plugins defining VERNAC EXTEND entries with the same name.
This happens currently with equations and quickchick that both define a Derive
command, leading to the impossibility of requiring both at the same time.

stm/stm.ml

@@ -126,13 +126,7 @@ let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr
 (* Commands piercing opaque *)
 let may_pierce_opaque = function
   | VernacSynPure (VernacPrint _) -> true
-  | VernacSynterp (VernacExtend (("Extraction",_), _)
-    | VernacExtend (("SeparateExtraction",_), _)
-    | VernacExtend (("ExtractionLibrary",_), _)
-    | VernacExtend (("RecursiveExtractionLibrary",_), _)
-    | VernacExtend (("ExtractionConstant",_), _)
-    | VernacExtend (("ExtractionInlinedConstant",_), _)
-    | VernacExtend (("ExtractionInductive",_), _)) -> true
+  | VernacSynterp (VernacExtend ({ ext_plugin = "coq-core.plugins.extraction" }, _)) -> true
   | _ -> false
 
 type depth = int

vernac/egramml.ml

@@ -82,7 +82,7 @@ let get_extend_vernac_rule s =
 
 let declare_vernac_command_grammar ~allow_override s nt gl =
   let () = if not allow_override && Hashtbl.mem vernac_exts s
-    then CErrors.anomaly Pp.(str "bad vernac extend: " ++ str (fst s) ++ str ", " ++ int (snd s))
+    then CErrors.anomaly Pp.(str "bad vernac extend: " ++ str s.ext_entry ++ str ", " ++ int s.ext_index)
   in
   let nt = Option.default Pvernac.Vernac_.command nt in
   Hashtbl.add vernac_exts s (nt, gl)

vernac/ppvernac.ml

@@ -686,7 +686,7 @@ let pr_using e =
 let pr_extend s cl =
   let pr_arg a =
     try pr_gen a
-    with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
+    with Failure _ -> str "<error in " ++ str s.ext_entry ++ str ">" in
   try
     let rl = Egramml.get_extend_vernac_rule s in
     let rec aux rl cl =
@@ -697,7 +697,7 @@ let pr_extend s cl =
       | _ -> assert false in
     hov 1 (pr_sequence identity (aux rl cl))
   with Not_found ->
-    hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+    hov 1 (str "TODO(" ++ str s.ext_entry ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
 let pr_synpure_vernac_expr v =
   let return = tag_vernac v in

vernac/vernac_classifier.ml

@@ -84,7 +84,7 @@ let classify_vernac e =
     | VernacLoad _ -> VtSideff ([], VtNow)
     | VernacExtend (s,l) ->
         try Vernacextend.get_vernac_classifier s l
-        with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
+        with Not_found -> anomaly(str"No classifier for"++spc()++str s.ext_entry ++str".")
   in
   let static_pure_classifier ~atts e = match e with
     (* Qed *)

vernac/vernacexpr.mli

@@ -327,13 +327,16 @@ type arguments_modifier =
   | `ReductionNeverUnfold
   | `Rename ]
 
-type extend_name =
-  (* Name of the vernac entry where the tactic is defined, typically found
+type extend_name = {
+  ext_plugin : string;
+  (** Name of the plugin where the extension is defined as per DECLARE PLUGIN *)
+  ext_entry : string;
+  (** Name of the vernac entry where the tactic is defined, typically found
      after the VERNAC EXTEND statement in the source. *)
-  string *
+  ext_index : int;
   (* Index of the extension in the VERNAC EXTEND statement. Each parsing branch
      is given an offset, starting from zero. *)
-  int
+}
 
 type discharge = DoDischarge | NoDischarge
 

vernac/vernacextend.ml

@@ -68,7 +68,7 @@ let vinterp_map s =
     Hashtbl.find vernac_tab s
   with Not_found ->
     user_err
-      (str"Cannot find vernac command " ++ str (fst s) ++ str".")
+      (str"Cannot find vernac command " ++ str s.ext_entry ++ str".")
 
 let warn_deprecated_command =
   let open CWarnings in
@@ -95,13 +95,24 @@ let type_vernac opn converted_args ?loc ~atts =
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 (** Classifiers  *)
-let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+module StringPair =
+struct
+  type t = string * string
+  let compare (s1, s2) (t1, t2) =
+    let c = String.compare s1 t1 in
+    if Int.equal c 0 then String.compare s2 t2 else c
+end
 
-let get_vernac_classifier (name, i) args =
-  (String.Map.find name !classifiers).(i) args
+module StringPairMap = Map.Make(StringPair)
+
+let classifiers : classifier array StringPairMap.t ref = ref StringPairMap.empty
+
+let get_vernac_classifier e args =
+  let open Vernacexpr in
+  (StringPairMap.find (e.ext_plugin, e.ext_entry) !classifiers).(e.ext_index) args
 
 let declare_vernac_classifier name f =
-  classifiers := String.Map.add name f !classifiers
+  classifiers := StringPairMap.add name f !classifiers
 
 let classify_as_query = VtQuery
 let classify_as_sideeff = VtSideff ([], VtLater)
@@ -173,10 +184,10 @@ let declare_dynamic_vernac_extend ~command ?entry ~depr cl ty f =
   let cl = untype_classifier ty cl in
   let f = untype_command ty f in
   let r = untype_grammar ty in
-  let ext = command, 0 in
+  let ext = { command with Vernacexpr.ext_index = 0 } in
   vinterp_add depr ext f;
   Egramml.declare_vernac_command_grammar ~allow_override:true ext entry r;
-  declare_vernac_classifier command [|cl|];
+  declare_vernac_classifier (ext.ext_plugin, ext.ext_entry) [|cl|];
   ext
 
 let is_static_linking_done = ref false
@@ -215,26 +226,28 @@ let static_vernac_extend ~plugin ~command ?classifier ?entry ext =
       CErrors.user_err (Pp.strbrk msg)
   in
   let cl = Array.map_of_list get_classifier ext in
+  let ext_plugin = Option.default "__" plugin in
   let iter i (TyML (depr, ty, f, _)) =
     let f = untype_command ty f in
     let r = untype_grammar ty in
-    let () = vinterp_add depr (command, i) f in
-    let () = Egramml.declare_vernac_command_grammar ~allow_override:false (command, i) entry r in
+    let ext = Vernacexpr.{ ext_plugin; ext_entry = command; ext_index = i } in
+    let () = vinterp_add depr ext f in
+    let () = Egramml.declare_vernac_command_grammar ~allow_override:false ext entry r in
     let () = match plugin with
       | None ->
         let () =
           if !is_static_linking_done
           then CErrors.anomaly
               Pp.(str "static_vernac_extend in dynlinked code must pass non-None plugin.")
         in
-        Egramml.extend_vernac_command_grammar ~undoable:false (command, i)
+        Egramml.extend_vernac_command_grammar ~undoable:false ext
       | Some plugin ->
         Mltop.add_init_function plugin (fun () ->
-            Egramml.extend_vernac_command_grammar ~undoable:true (command, i))
+            Egramml.extend_vernac_command_grammar ~undoable:true ext)
     in
     ()
   in
-  let () = declare_vernac_classifier command cl in
+  let () = declare_vernac_classifier (ext_plugin, command) cl in
   let () = List.iteri iter ext in
   ()
 

vernac/vernacextend.mli

@@ -122,7 +122,7 @@ val static_linking_done : unit -> unit
     enabled it.
 *)
 val declare_dynamic_vernac_extend
-  : command:string
+  : command:Vernacexpr.extend_name
   -> ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t
   -> depr:bool
   -> 's (* classifier *)