Uniformizing generic argument types.

Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.

This has various advantages:

- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.

Documenting a bit Genarg b.t.w.

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

3 files changed, 11 insertions, 15 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 70338c52b5..291fabdb6e 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -100,27 +100,25 @@ let proof_instr = Gram.entry_create "proofmode:instr"
 (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
 
 (* [Genarg.create_arg] creates a new embedding into Genarg. *)
-let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) =
+let wit_proof_instr =
   Genarg.create_arg None "proof_instr"
 let _ = Tacintern.add_intern_genarg "proof_instr"
   begin fun e x -> (* declares the globalisation function *)
-    Genarg.in_gen globwit_proof_instr 
-      (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x))
+    Genarg.in_gen (Genarg.glbwit wit_proof_instr)
+      (Decl_interp.intern_proof_instr e (Genarg.out_gen (Genarg.rawwit wit_proof_instr) x))
   end
 let _ = Tacinterp.add_interp_genarg "proof_instr"
   begin fun ist gl x -> (* declares the interpretation function *)
     Tacmach.project gl ,
-    Genarg.in_gen wit_proof_instr 
-      (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x))
+    Genarg.in_gen (Genarg.topwit wit_proof_instr)
+      (interp_proof_instr ist gl (Genarg.out_gen (Genarg.glbwit wit_proof_instr) x))
   end
 (* declares the substitution function, irrelevant in our case : *)
 let _ = Tacsubst.add_genarg_subst "proof_instr" (fun _ x -> x)
 
 
-let _ = Pptactic.declare_extra_genarg_pprule
-  (rawwit_proof_instr, pr_raw_proof_instr)
-  (globwit_proof_instr, pr_glob_proof_instr)
-  (wit_proof_instr, pr_proof_instr)
+let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
+  pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
 
 (* We use the VERNAC EXTEND facility with a custom non-terminal
     to populate [proof_mode] with a new toplevel interpreter.
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 088b4a0cde..8b90824fd2 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -151,11 +151,9 @@ GEXTEND Gram
     ;
 
   END
-type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located, 'a) Genarg.abstract_argument_type
+type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
 
-let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
-  (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
-  (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) =
+let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
   Genarg.create_arg None "function_rec_definition_loc"
 VERNAC COMMAND EXTEND Function
    ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index b6b69ec2d0..5556912ebb 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -129,8 +129,8 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,Id.of_string"t"),None);
-   Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
+  [Genarg.in_gen (Genarg.glbwit Genarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
+   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Genarg.wit_ref)) l])))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)