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, 5 insertions, 6 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a90c565f1..8f570af7e 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -105,12 +105,11 @@ let wit_proof_instr =
   let subst _ x = x in
   let glob ist v = (ist, Decl_interp.intern_proof_instr ist v) in
   let interp ist gl x = (Tacmach.project gl, interp_proof_instr ist gl x) in
-  let arg = { Genarg.default_arg0 name with
-    Genarg.arg0_subst = subst;
-    Genarg.arg0_glob = glob;
-    Genarg.arg0_interp = interp;
-  } in
-  Genarg.make0 None name arg
+  let arg = Genarg.make0 None name in
+  let () = Genintern.register_intern0 arg glob in
+  let () = Genintern.register_subst0 arg subst in
+  let () = Geninterp.register_interp0 arg interp in
+  arg
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr