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, 19 insertions, 16 deletions

diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7fc3ac8a5..cd4d777d6 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -15,20 +15,19 @@ open Termops
 open Glob_term
 open Misctypes
 
-val rawwit_orient : bool raw_abstract_argument_type
-val globwit_orient : bool glob_abstract_argument_type
-val wit_orient : bool typed_abstract_argument_type
+val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
 val pr_orient : bool -> Pp.std_ppcmds
 
 val occurrences : (int list or_var) Pcoq.Gram.entry
-val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
-val wit_occurrences : (int list) typed_abstract_argument_type
+val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
 val occurrences_of : int list -> Locus.occurrences
 
-val rawwit_glob : constr_expr raw_abstract_argument_type
-val wit_glob : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type
+val wit_glob :
+  (constr_expr,
+  Genarg.glob_constr_and_expr,
+  Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 val glob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
@@ -36,22 +35,27 @@ type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 type loc_place = Id.t Loc.located gen_place
 type place = Id.t gen_place
 
-val rawwit_hloc : loc_place raw_abstract_argument_type
-val wit_hloc : place typed_abstract_argument_type
+val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
 val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
 val in_arg_hyp:  (Names.Id.t Loc.located list option * bool)  Pcoq.Gram.entry
-val globwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) glob_abstract_argument_type
-val rawwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) raw_abstract_argument_type
-val wit_in_arg_hyp : (Names.Id.t list option * bool) typed_abstract_argument_type
+
+val wit_in_arg_hyp :
+  ((Names.Id.t Loc.located list option * bool),
+  (Names.Id.t Loc.located list option * bool),
+  (Names.Id.t list option * bool)) Genarg.genarg_type
+
 val raw_in_arg_hyp_to_clause : (Names.Id.t Loc.located list option * bool) -> Locus.clause
 val glob_in_arg_hyp_to_clause :  (Names.Id.t list option * bool)  -> Locus.clause
 val pr_in_arg_hyp : (Names.Id.t list option * bool) -> Pp.std_ppcmds
 
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
-val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
-val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
+val wit_by_arg_tac :
+  (raw_tactic_expr option,
+  glob_tactic_expr option,
+  glob_tactic_expr option) Genarg.genarg_type
+
 val pr_by_arg_tac : 
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
@@ -60,5 +64,4 @@ val pr_by_arg_tac :
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
-val rawwit_retroknowledge_field :  Retroknowledge.field raw_abstract_argument_type
-val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type
+val wit_retroknowledge_field : Retroknowledge.field Genarg.uniform_genarg_type