Simplifying and uniformizing the implementation of tactic notations.

This branch mainly provides two features:

1. The resolution of tactic notation scopes is not tied to a hardwired Pcoq
registration anymore. We expose instead an API to interpret names as a given
generic argument, effectively reversing the logical dependency between parsing
entries and generic arguments.

2. ML tactics do not declare their own notation system anymore. They rely instead
on plain tactic notations, except for a little hack due to the way we currently
interpret toplevel values.

2 files changed, 27 insertions, 17 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 2ef30f299b..19b6e1b5f6 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -45,26 +45,30 @@ let make_fun_clauses loc s l =
   let map c = Compat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
+let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >>
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+  let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  let arg = get_argt <:expr< Constrarg.wit_tactic >> in
+  <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
+
 let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
   | ExtNonTerminal (g, id) ->
-    let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
-      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key base g$ >>
+    <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
 
-let make_one_printing_rule (pt,_,e) =
-  let level = mlexpr_of_int 0 in (* only level 0 supported here *)
-  let loc = MLast.loc_of_expr e in
-  let prods = mlexpr_of_list make_prod_item pt in
-  <:expr< { Pptactic.pptac_level = $level$;
-            pptac_prods = $prods$ } >>
-
-let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
-
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
@@ -118,15 +122,13 @@ let declare_tactic loc s c cl = match cl with
       TacML tactic. *)
   let entry = mlexpr_of_string s in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
       try do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
-        Mltop.declare_cache_obj $obj$ $plugin_name$;
-        Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); }
+        Mltop.declare_cache_obj $obj$ $plugin_name$; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
           (Pp.app
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index aedaead71a..0d4bec69d5 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -102,6 +102,14 @@ let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
+let make_prod_item = function
+  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | ExtNonTerminal (g, id) ->
+    let nt = type_of_user_symbol g in
+    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
+      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
+      $mlexpr_of_prod_entry_key base g$ >>
+
 let mlexpr_of_clause cl =
   let mkexpr { r_head = a; r_patt = b; } = match a with
   | None -> mlexpr_of_list make_prod_item b