Put all plugins behind an "API".

4 files changed, 46 insertions, 46 deletions

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 5068ba8a6..36b9d612a 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -46,17 +46,17 @@ let make_act loc act pil =
   make (List.rev pil)
 
 let make_prod_item = function
-  | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
+  | ExtTerminal s -> <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $mlexpr_of_string s$) >>
   | ExtNonTerminal (g, _) ->
     let base s = <:expr< $lid:s$ >> in
     mlexpr_of_prod_entry_key base g
 
 let rec make_prod = function
-| [] -> <:expr< Extend.Stop >>
-| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >>
+| [] -> <:expr< Grammar_API.Extend.Stop >>
+| item :: prods -> <:expr< Grammar_API.Extend.Next $make_prod prods$ $make_prod_item item$ >>
 
 let make_rule loc (prods,act) =
-  <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >>
+  <:expr< Grammar_API.Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >>
 
 let is_ident x = function
 | <:expr< $lid:s$ >> -> (s : string) = x
@@ -67,7 +67,7 @@ let make_extend loc s cl wit = match cl with
   (** Special handling of identity arguments by not redeclaring an entry *)
   <:str_item<
     value $lid:s$ =
-      let () = Pcoq.register_grammar $wit$ $lid:e$ in
+      let () = Grammar_API.Pcoq.register_grammar $wit$ $lid:e$ in
       $lid:e$
   >>
 | _ ->
@@ -75,8 +75,8 @@ let make_extend loc s cl wit = match cl with
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
   <:str_item<
     value $lid:s$ =
-      let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in
-      let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in
+      let $lid:s$ = Grammar_API.Pcoq.create_generic_entry Grammar_API.Pcoq.utactic $se$ (Genarg.rawwit $wit$) in
+      let () = Grammar_API.Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in
       $lid:s$ >>
 
 let warning_redundant prefix s =
@@ -127,7 +127,7 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       begin match globtyp with
       | None ->
         let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
-        <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >>
+        <:expr< fun ist v -> API.Ftactic.return (API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v) >>
       | Some globtyp ->
         <:expr< fun ist x ->
           Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >>
@@ -137,10 +137,10 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
       <:expr<
         let f = $lid:f$ in
-        fun ist v -> Ftactic.nf_enter (fun gl ->
-          let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
-          let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in
-          Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v)
+        fun ist v -> API.Ftactic.nf_enter (fun gl ->
+          let (sigma, v) = API.Tacmach.New.of_old (fun gl -> f ist gl v) gl in
+          let v = API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v in
+          API.Proofview.tclTHEN (API.Proofview.Unsafe.tclEVARS sigma) (API.Ftactic.return v)
         )
       >> in
   let subst = match h with
@@ -156,15 +156,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
     | Some f -> <:expr< $lid:f$>> in
   let dyn = match typ with
   | None -> <:expr< None >>
-  | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >>
+  | Some typ -> <:expr< Some (API.Geninterp.val_tag $make_topwit loc typ$) >>
   in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   declare_str_items loc
    [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>;
-     <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
-     <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
-     <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
-     <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>;
+     <:str_item< Grammar_API.Genintern.register_intern0 $wit$ $glob$ >>;
+     <:str_item< Grammar_API.Genintern.register_subst0 $wit$ $subst$ >>;
+     <:str_item< API.Geninterp.register_interp0 $wit$ $interp$ >>;
+     <:str_item< API.Geninterp.register_val0 $wit$ $dyn$ >>;
      make_extend loc s cl wit;
      <:str_item< do {
       Pptactic.declare_extra_genarg_pprule
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 87262e1c8..7d309cf0d 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -60,20 +60,20 @@ let mlexpr_of_name f = function
   | None -> <:expr< Anonymous >>
   | Some e -> <:expr< Name $f e$ >>
 
-let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
+let symbol_of_string s = <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $str:s$) >>
 
 let rec mlexpr_of_prod_entry_key f = function
-  | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
-  | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
-  | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
-  | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
-  | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Uentry e -> <:expr< Extend.Aentry $f e$ >>
+  | Ulist1 s -> <:expr< Grammar_API.Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+  | Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
+  | Ulist0 s -> <:expr< Grammar_API.Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+  | Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
+  | Uopt s -> <:expr< Grammar_API.Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
+  | Uentry e -> <:expr< Grammar_API.Extend.Aentry ($f e$) >>
   | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (e = "tactic");
-    if l = 5 then <:expr< Extend.Aentry (Pltac.binder_tactic) >>
-    else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
+    if l = 5 then <:expr< Grammar_API.Extend.Aentry Pltac.binder_tactic >>
+    else <:expr< Grammar_API.Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 8e3dccf47..8f3f7a9de 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -25,7 +25,7 @@ let plugin_name = <:expr< __coq_plugin_name >>
 let mlexpr_of_ident id =
   (** Workaround for badly-designed generic arguments lacking a closure *)
   let id = "$" ^ id in
-  <:expr< Names.Id.of_string_soft $str:id$ >>
+  <:expr< API.Names.Id.of_string_soft $str:id$ >>
 
 let rec make_patt = function
   | [] -> <:patt< [] >>
@@ -57,18 +57,18 @@ let make_fun_clauses loc s l =
 let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >>
 
 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$ >>
+| Ulist1 s -> <:expr< Grammar_API.Extend.Ulist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Grammar_API.Extend.Ulist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Grammar_API.Extend.Uopt $mlexpr_of_symbol s$ >>
 | Uentry e ->
   let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+  <:expr< Grammar_API.Extend.Uentry (Genarg.ArgT.Any $arg$) >>
 | Uentryl (e, l) ->
   assert (e = "tactic");
   let arg = get_argt <:expr< Tacarg.wit_tactic >> in
-  <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
+  <:expr< Grammar_API.Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
@@ -113,12 +113,12 @@ let declare_tactic loc tacname ~level classification clause = match clause with
       the ML tactic retrieves its arguments in the [ist] environment instead.
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
   let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in
-  let name = <:expr< Names.Id.of_string $name$ >> in
+  let name = <:expr< API.Names.Id.of_string $name$ >> in
   declare_str_items loc
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac True False $name$ $body$ in
       let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in
-      Mltop.declare_cache_obj obj $plugin_name$ } >>
+      API.Mltop.declare_cache_obj obj $plugin_name$ } >>
     ]
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
@@ -131,7 +131,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with
   declare_str_items loc
     [ <:str_item< do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
-        Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
+        Grammar_API.Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
     ]
 
 open Pcaml
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 798b46523..6f0e9b7cf 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -100,12 +100,12 @@ let make_fun_classifiers loc s c l =
   mlexpr_of_list (fun x -> x) cl
 
 let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | ExtTerminal s -> <:expr< Grammar_API.Egramml.GramTerminal $str:s$ >>
   | ExtNonTerminal (g, ido) ->
     let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
+    let base s = <:expr< Grammar_API.Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
     let typ = match ido with None -> None | Some _ -> Some nt in
-      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
+      <:expr< Grammar_API.Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
       $mlexpr_of_prod_entry_key base g$ ) ) >>
 
 let mlexpr_of_clause cl =
@@ -122,9 +122,9 @@ let declare_command loc s c nt cl =
   let classl = make_fun_classifiers loc s c cl in
   declare_str_items loc
     [ <:str_item< do {
-        CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
-        CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
-	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
+        CList.iteri (fun i (depr, f) -> Grammar_API.Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
+        CList.iteri (fun i f -> API.Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
+	CList.iteri (fun i r -> Grammar_API.Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
       } >> ]
 
 open Pcaml
@@ -143,16 +143,16 @@ EXTEND
       | "DECLARE"; "PLUGIN"; name = STRING ->
         declare_str_items loc [
           <:str_item< value __coq_plugin_name = $str:name$ >>;
-          <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
+          <:str_item< value _ = Grammar_API.Mltop.add_known_module __coq_plugin_name >>;
         ]
       ] ]
   ;
   classification:
     [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >>
       | "CLASSIFIED"; "AS"; "SIDEFF" ->
-          <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >>
+          <:expr< fun _ -> API.Vernac_classifier.classify_as_sideeff >>
       | "CLASSIFIED"; "AS"; "QUERY" ->
-          <:expr< fun _ -> Vernac_classifier.classify_as_query >>
+          <:expr< fun _ -> API.Vernac_classifier.classify_as_query >>
     ] ]
   ;
   deprecation: