Splitted up Genarg in four different levels:

1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
   functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.

The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 9 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index dffca2c62..fd18dfdf1 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -186,21 +186,16 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
             (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
       end
     | Some f -> <:expr< $lid:f$>> in
-  let defs = [
-    <:patt< Genarg.arg0_subst >>, subst;
-    <:patt< Genarg.arg0_glob >>, glob;
-    <:patt< Genarg.arg0_interp >>, interp;
-  ] in
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   let rawwit = <:expr< Genarg.rawwit $wit$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
   let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
   declare_str_items loc
-   [ <:str_item<
-      value ($lid:"wit_"^s$) =
-        let arg = { (Genarg.default_arg0 $se$) with $list:defs$ } in
-      Genarg.make0 $default_value$ $se$ arg >>;
+   [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $default_value$ $se$ >>;
+     <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
+     <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
+     <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
      <:str_item< do {