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

1 files changed, 7 insertions, 9 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.