Suppression des local_constraints, des ctxtty et du focus.

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

20 files changed, 196 insertions, 199 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1ecb4ce2d..7b7ef647d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -382,9 +382,9 @@ let push_history_pattern n current cont =
   of variables).
 
 *)
-type 'a pattern_matching_problem =
+type pattern_matching_problem =
     { env      : env;
-      isevars  : 'a evar_defs;
+      isevars  : evar_defs;
       pred     : predicate_signature option;
       tomatch  : tomatch_stack;
       history  : pattern_continuation;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 3126198f9..193882ba0 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -32,16 +32,16 @@ exception PatternMatchingError of env * pattern_matching_error
 (* Used for old cases in pretyping *)
 
 val branch_scheme : 
-  env -> 'a evar_defs -> bool -> inductive * constr list -> constr array
+  env -> evar_defs -> bool -> inductive * constr list -> constr array
 
-val pred_case_ml_onebranch : loc -> env -> 'c evar_map -> bool ->
+val pred_case_ml_onebranch : loc -> env -> evar_map -> bool ->
   inductive_type -> int * unsafe_judgment -> constr 
 
 (* Compilation of pattern-matching. *)
 
 val compile_cases :
   loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment)
-  * 'a evar_defs -> type_constraint -> env ->
+  * evar_defs -> type_constraint -> env ->
     rawconstr option * rawconstr list *
     (loc * identifier list * cases_pattern list * rawconstr) list ->
     unsafe_judgment
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index eaeb25bc0..b8817ae0e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -60,7 +60,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 val constructor_at_head : constr -> cl_typ * int
 
 (* raises [Not_found] if not convertible to a class *)
-val class_of : env -> 'c evar_map -> constr -> constr * cl_index
+val class_of : env -> evar_map -> constr -> constr * cl_index
 
 val class_args_of : constr -> constr list
 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 1c07a7ed3..4ca3ba987 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -22,19 +22,19 @@ open Evarutil
    inserts a coercion into [j], if needed, in such a way it gets as
    type a product; it returns [j] if no coercion is applicable *)
 val inh_app_fun :
-  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+  env -> evar_defs -> unsafe_judgment -> unsafe_judgment
 
 (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
    inserts a coercion into [j], if needed, in such a way it gets as
    type a sort; it fails if no coercion is applicable *)
 val inh_coerce_to_sort :
-  env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
+  env -> evar_defs -> unsafe_judgment -> unsafe_type_judgment
 
 (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
    [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
    [j.uj_type] are convertible; it fails if no coercion is applicable *)
 val inh_conv_coerce_to : Rawterm.loc -> 
-  env -> 'a evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
+  env -> evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
 
 (*i
 (* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 06a866f48..24830b30a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,13 +16,13 @@ open Reductionops
 open Evarutil
 (*i*)
 
-val the_conv_x : env -> 'a evar_defs -> constr -> constr -> bool
+val the_conv_x : env -> evar_defs -> constr -> constr -> bool
 
-val the_conv_x_leq : env -> 'a evar_defs -> constr -> constr -> bool
+val the_conv_x_leq : env -> evar_defs -> constr -> constr -> bool
 
 (*i For debugging *)
-val evar_conv_x : env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool
+val evar_conv_x : env -> evar_defs -> conv_pb -> constr -> constr -> bool
 val evar_eqappr_x : 
-  env -> 'a evar_defs ->
+  env -> evar_defs ->
     conv_pb -> constr * constr list -> constr * constr list -> bool
 (*i*)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 533292ec7..d4a341d1b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -115,7 +115,7 @@ let new_isevar_sign env sigma typ instance =
     error "new_isevar_sign: two vars have the same name";
   let newev = new_evar() in
   let info = { evar_concl = typ; evar_hyps = sign; 
-	       evar_body = Evar_empty; evar_info = None } in
+	       evar_body = Evar_empty } in
   (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))
 
 (* We don't try to guess in which sort the type should be defined, since
@@ -204,8 +204,8 @@ let do_restrict_hyps sigma ev args =
  *------------------------------------*)
 
 type evar_constraint = conv_pb * constr * constr
-type 'a evar_defs =
-    { mutable evars : 'a Evd.evar_map;
+type evar_defs =
+    { mutable evars : Evd.evar_map;
       mutable conv_pbs : evar_constraint list }
 
 let create_evar_defs evd = { evars=evd; conv_pbs=[] }
@@ -464,7 +464,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in
   let newev = new_evar () in
   let info = { evar_concl = evd.evar_concl; evar_hyps = nsign;
-	       evar_body = Evar_empty; evar_info = None } in
+	       evar_body = Evar_empty } in
   isevars.evars <-
     Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs));
   [ev]
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 01a2437b2..66e48664a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -22,49 +22,49 @@ open Reductionops
 (* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
 (* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
 
-val nf_evar : 'a evar_map -> constr -> constr
-val j_nf_evar : 'a evar_map -> unsafe_judgment -> unsafe_judgment
+val nf_evar :  evar_map -> constr -> constr
+val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
-  'a evar_map -> unsafe_judgment list -> unsafe_judgment list
+   evar_map -> unsafe_judgment list -> unsafe_judgment list
 val jv_nf_evar :
-  'a evar_map -> unsafe_judgment array -> unsafe_judgment array
+   evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_evar :
-  'a evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 (* Replacing all evars *)
 exception Uninstantiated_evar of int
-val whd_ise : 'a evar_map -> constr -> constr
-val whd_castappevar : 'a evar_map -> constr -> constr
+val whd_ise :  evar_map -> constr -> constr
+val whd_castappevar :  evar_map -> constr -> constr
 
 (* Creating new existential variables *)
 val new_evar : unit -> evar
 val new_evar_in_sign : env -> constr
 
-val evar_env : 'a evar_info -> env
+val evar_env :  evar_info -> env
 
-type 'a evar_defs
-val evars_of : 'a evar_defs -> 'a evar_map
-val create_evar_defs : 'a evar_map -> 'a evar_defs
-val evars_reset_evd : 'a evar_map -> 'a evar_defs -> unit
+type evar_defs
+val evars_of :  evar_defs ->  evar_map
+val create_evar_defs :  evar_map ->  evar_defs
+val evars_reset_evd :  evar_map ->  evar_defs -> unit
 
 type evar_constraint = conv_pb * constr * constr
-val add_conv_pb : 'a evar_defs -> evar_constraint -> unit
+val add_conv_pb :  evar_defs -> evar_constraint -> unit
 
-val is_defined_evar : 'a evar_defs -> existential -> bool
-val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
-val ise_undefined : 'a evar_defs -> constr -> bool
-val has_undefined_isevars : 'a evar_defs -> constr -> bool
+val is_defined_evar :  evar_defs -> existential -> bool
+val ise_try :  evar_defs -> (unit -> bool) list -> bool
+val ise_undefined :  evar_defs -> constr -> bool
+val has_undefined_isevars :  evar_defs -> constr -> bool
 
-val new_isevar : 'a evar_defs -> env -> constr -> constr
+val new_isevar :  evar_defs -> env -> constr -> constr
 
 val is_eliminator : constr -> bool
-val head_is_embedded_evar : 'a evar_defs -> constr -> bool
+val head_is_embedded_evar :  evar_defs -> constr -> bool
 val solve_simple_eqn :
-  (env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool)
-  -> env -> 'a evar_defs -> conv_pb * existential * constr -> bool
+  (env ->  evar_defs -> conv_pb -> constr -> constr -> bool)
+  -> env ->  evar_defs -> conv_pb * existential * constr -> bool
 
-val define_evar_as_arrow : 'a evar_map -> existential -> 'a evar_map * types
-val define_evar_as_sort : 'a evar_map -> existential -> 'a evar_map * sorts
+val define_evar_as_arrow :  evar_map -> existential ->  evar_map * types
+val define_evar_as_sort :  evar_map -> existential ->  evar_map * sorts
 
 (* Value/Type constraints *)
 
@@ -81,7 +81,7 @@ val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
 val split_tycon :
-  Rawterm.loc -> env -> 'a evar_defs -> type_constraint -> 
+  Rawterm.loc -> env ->  evar_defs -> type_constraint -> 
     type_constraint * type_constraint
 
 val valcon_of_tycon : type_constraint -> val_constraint
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a80f21b52..ee99bfb4b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -21,13 +21,12 @@ type evar_body =
   | Evar_empty 
   | Evar_defined of constr
 
-type 'a evar_info = {
+type evar_info = {
   evar_concl : constr;
   evar_hyps : named_context;
-  evar_body : evar_body;
-  evar_info : 'a option }
+  evar_body : evar_body}
 
-type 'a evar_map = 'a evar_info Intmap.t
+type evar_map = evar_info Intmap.t
 
 let empty = Intmap.empty
 
@@ -45,8 +44,7 @@ let define evd ev body =
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
       evar_hyps = oldinfo.evar_hyps;
-      evar_body = Evar_defined body;
-      evar_info = oldinfo.evar_info } 
+      evar_body = Evar_defined body} 
   in
   match oldinfo.evar_body with
     | Evar_empty -> Intmap.add ev newinfo evd
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f6192c7e5..f6a2bb43a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -26,32 +26,31 @@ type evar_body =
   | Evar_empty 
   | Evar_defined of constr
 
-type 'a evar_info = {
+type evar_info = {
   evar_concl : constr;
   evar_hyps : named_context;
-  evar_body : evar_body;
-  evar_info : 'a option }
+  evar_body : evar_body}
 
-type 'a evar_map
+type evar_map
 
-val empty : 'a evar_map
+val empty : evar_map
 
-val add : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
+val add : evar_map -> evar -> evar_info -> evar_map
 
-val dom : 'a evar_map -> evar list
-val map : 'a evar_map -> evar -> 'a evar_info
-val rmv : 'a evar_map -> evar -> 'a evar_map
-val remap : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
-val in_dom : 'a evar_map -> evar -> bool
-val to_list : 'a evar_map -> (evar * 'a evar_info) list
+val dom : evar_map -> evar list
+val map : evar_map -> evar -> evar_info
+val rmv : evar_map -> evar -> evar_map
+val remap : evar_map -> evar -> evar_info -> evar_map
+val in_dom : evar_map -> evar -> bool
+val to_list : evar_map -> (evar * evar_info) list
 
-val define : 'a evar_map -> evar -> constr -> 'a evar_map
+val define : evar_map -> evar -> constr -> evar_map
 
-val non_instantiated : 'a evar_map -> (evar * 'a evar_info) list
-val is_evar : 'a evar_map -> evar -> bool
+val non_instantiated : evar_map -> (evar * evar_info) list
+val is_evar : evar_map -> evar -> bool
 
-val is_defined : 'a evar_map -> evar -> bool
+val is_defined : evar_map -> evar -> bool
 
-val evar_body : 'a evar_info -> evar_body
+val evar_body : evar_info -> evar_body
 
 val id_of_existential : evar -> identifier
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 7e6dd8fa1..e28331848 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -21,30 +21,30 @@ open Evd
 
 (* These functions build elimination predicate for Case tactic *)
 
-val make_case_dep : env -> 'a evar_map -> inductive -> sorts_family -> constr
-val make_case_nodep : env -> 'a evar_map -> inductive -> sorts_family -> constr
-val make_case_gen : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr
+val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr
+val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
 
 (* This builds an elimination scheme associated (using the own arity
    of the inductive) *)
 
-val build_indrec : env -> 'a evar_map -> inductive -> constr
+val build_indrec : env -> evar_map -> inductive -> constr
 val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 
 (* This builds complex [Scheme] *)
 
 val build_mutual_indrec : 
-  env -> 'a evar_map ->
+  env -> evar_map ->
     (inductive * mutual_inductive_body * one_inductive_body
     * bool * sorts_family) list
     -> constr list
 
 (* These are for old Case/Match typing *)
 
-val type_rec_branches : bool -> env -> 'c evar_map -> inductive_type
+val type_rec_branches : bool -> env -> evar_map -> inductive_type
   -> unsafe_judgment -> constr -> constr array * constr
 val make_rec_branch_arg : 
-  env -> 'a evar_map ->
+  env -> evar_map ->
     int * ('b * constr) option array * int ->
     constr -> constructor_summary -> recarg list -> constr
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7ca5b8b1b..2174bf0e9 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -72,14 +72,14 @@ val build_branch_type :
 exception Induc
 val extract_mrectype : constr -> inductive * constr list
 val find_mrectype :
-  env -> 'a evar_map -> constr -> inductive * constr list
+  env -> evar_map -> constr -> inductive * constr list
 val find_rectype :
-  env -> 'a evar_map -> constr -> inductive_type
+  env -> evar_map -> constr -> inductive_type
 val find_inductive :
-  env -> 'a evar_map -> constr -> inductive * constr list
+  env -> evar_map -> constr -> inductive * constr list
 val find_coinductive :
   env ->
-  'a evar_map -> constr -> inductive * constr list
+  evar_map -> constr -> inductive * constr list
 val type_case_branches_with_names :
   env -> inductive * constr list -> unsafe_judgment -> constr ->
     types array * types
diff --git a/pretyping/instantiate.mli b/pretyping/instantiate.mli
index 4f4184769..e66471bb5 100644
--- a/pretyping/instantiate.mli
+++ b/pretyping/instantiate.mli
@@ -20,6 +20,6 @@ open Environ
 no body and [Not_found] if it does not exist in [sigma] *)
 
 exception NotInstantiatedEvar
-val existential_value : 'a evar_map -> existential -> constr
-val existential_type : 'a evar_map -> existential -> types
-val existential_opt_value : 'a evar_map -> existential -> constr option
+val existential_value : evar_map -> existential -> constr
+val existential_type : evar_map -> existential -> types
+val existential_opt_value : evar_map -> existential -> constr option
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 4a477b8e5..cc36b260a 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -82,7 +82,7 @@ val is_matching      :
    increasing order based on the numbers given in the pattern *)
 
 val matches_conv :
-  env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
+  env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
 
 (* To skip to the next occurrence *)
 exception NextOccurrence of int
@@ -95,4 +95,4 @@ val sub_match :
    up to conversion for constants in patterns *)
 
 val is_matching_conv :
-  env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool
+  env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 11bf5b531..5d04c5047 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -39,65 +39,65 @@ type pretype_error =
 exception PretypeError of env * pretype_error
 
 (* Presenting terms without solved evars *)
-val nf_evar : 'a Evd.evar_map -> constr -> constr
-val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val nf_evar :  Evd.evar_map -> constr -> constr
+val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
-  'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+   Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
 val jv_nf_evar :
-  'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+   Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_evar :
-  'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+   Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 
 (* Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> 'a Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  loc -> env ->  Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc : 
-  loc -> env -> 'a Evd.evar_map ->
+  loc -> env ->  Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc : 
-  loc -> env -> 'a Evd.evar_map -> int * constr * constr -> 
+  loc -> env ->  Evd.evar_map -> int * constr * constr -> 
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_find_case_type_loc :
-  loc -> env -> 'a Evd.evar_map -> constr -> 'b
+  loc -> env ->  Evd.evar_map -> constr -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env -> 'a Evd.evar_map -> unsafe_judgment -> 'b
+  loc -> env ->  Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc : 
-  loc -> env -> 'a Evd.evar_map ->
+  loc -> env ->  Evd.evar_map ->
       constr -> int -> constr -> constr -> 'b
 
 val error_number_branches_loc : 
-  loc -> env -> 'a Evd.evar_map ->
+  loc -> env ->  Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env -> 'a Evd.evar_map ->
+  loc -> env ->  Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 (*s Implicit arguments synthesis errors *)
 
-val error_occur_check : env -> 'a Evd.evar_map -> int -> constr -> 'b
+val error_occur_check : env ->  Evd.evar_map -> int -> constr -> 'b
 
-val error_not_clean : env -> 'a Evd.evar_map -> int -> constr -> 'b
+val error_not_clean : env ->  Evd.evar_map -> int -> constr -> 'b
 
 (*s Ml Case errors *)
 
 val error_ml_case_loc :
-  loc -> env -> 'a Evd.evar_map ->
+  loc -> env ->  Evd.evar_map ->
       ml_case_error -> inductive_type -> unsafe_judgment -> 'b
 
 (*s Pretyping errors *)
 
 val error_unexpected_type_loc :
-  loc -> env -> 'a Evd.evar_map -> constr -> constr -> 'b
+  loc -> env ->  Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env -> 'a Evd.evar_map -> constr -> 'b
+  loc -> env ->  Evd.evar_map -> constr -> 'b
 
 (*s Error in conversion from AST to rawterms *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index bf48e305f..91a8da2c7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -36,7 +36,7 @@ type open_constr = (existential * types) list * constr
    typopt : is not None, this is the expected type for raw (used to define evars)
 *)
 val understand_gen :
-  'a evar_map -> env -> var_map -> meta_map 
+  evar_map -> env -> var_map -> meta_map 
     -> expected_type:(constr option) -> rawconstr -> constr
 
 
@@ -44,20 +44,20 @@ val understand_gen :
    unresolved holes into metas. Returns also the typing context of
    these metas. Work as [understand_gen] for the rest. *)
 val understand_gen_tcc :
-  'a evar_map -> env -> var_map -> meta_map 
+  evar_map -> env -> var_map -> meta_map 
     -> constr option -> rawconstr -> open_constr
 
 (* Standard call to get a constr from a rawconstr, resolving implicit args *)
-val understand : 'a evar_map -> env -> rawconstr -> constr
+val understand : evar_map -> env -> rawconstr -> constr
 
 (* Idem but the rawconstr is intended to be a type *)
-val understand_type : 'a evar_map -> env -> rawconstr -> constr
+val understand_type : evar_map -> env -> rawconstr -> constr
 
 (* Idem but returns the judgment of the understood term *)
-val understand_judgment : 'a evar_map -> env -> rawconstr -> unsafe_judgment
+val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
 (* Idem but returns the judgment of the understood type *)
-val understand_type_judgment : 'a evar_map -> env -> rawconstr 
+val understand_type_judgment : evar_map -> env -> rawconstr 
   -> unsafe_type_judgment
 
 (* To embed constr in rawconstr *)
@@ -69,10 +69,10 @@ val constr_out : Dyn.t -> constr
  * Unused outside, but useful for debugging
  *)
 val pretype : 
-  type_constraint -> env -> 'a evar_defs -> var_map -> meta_map ->
+  type_constraint -> env -> evar_defs -> var_map -> meta_map ->
     rawconstr -> unsafe_judgment
 
 val pretype_type : 
-  val_constraint -> env -> 'a evar_defs -> var_map -> meta_map ->
+  val_constraint -> env -> evar_defs -> var_map -> meta_map ->
     rawconstr -> unsafe_type_judgment
 (*i*)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a34c47c5a..410f8aa08 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -26,18 +26,18 @@ exception Elimconst
 (* The type of (machine) states (= lambda-bar-calculus' cuts) *) 
 type state = constr * constr stack
 
-type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
-type 'a reduction_function = 'a contextual_reduction_function
+type  contextual_reduction_function = env ->  evar_map -> constr -> constr
+type  reduction_function =  contextual_reduction_function
 type local_reduction_function = constr -> constr
 
-type 'a contextual_stack_reduction_function = 
-    env -> 'a evar_map -> constr -> constr * constr list
-type 'a stack_reduction_function = 'a contextual_stack_reduction_function
+type  contextual_stack_reduction_function = 
+    env ->  evar_map -> constr -> constr * constr list
+type  stack_reduction_function =  contextual_stack_reduction_function
 type local_stack_reduction_function = constr -> constr * constr list
 
-type 'a contextual_state_reduction_function = 
-    env -> 'a evar_map -> state -> state
-type 'a state_reduction_function = 'a contextual_state_reduction_function
+type  contextual_state_reduction_function = 
+    env ->  evar_map -> state -> state
+type  state_reduction_function =  contextual_state_reduction_function
 type local_state_reduction_function = state -> state
 
 (*************************************)
@@ -452,8 +452,8 @@ let fakey = Profile.declare_profile "fhnf_apply";;
 let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
 *)
 
-type 'a conversion_function = 
-    env -> 'a evar_map -> constr -> constr -> constraints
+type  conversion_function = 
+    env ->  evar_map -> constr -> constr -> constraints
 
 (* Conversion utility functions *)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 20c991032..8bd3ab489 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -23,18 +23,18 @@ exception Elimconst
 
 type state = constr * constr stack
 
-type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr
-type 'a reduction_function = 'a contextual_reduction_function
+type contextual_reduction_function = env -> evar_map -> constr -> constr
+type reduction_function = contextual_reduction_function
 type local_reduction_function = constr -> constr
 
-type 'a contextual_stack_reduction_function = 
-    env -> 'a evar_map -> constr -> constr * constr list
-type 'a stack_reduction_function = 'a contextual_stack_reduction_function
+type contextual_stack_reduction_function = 
+    env -> evar_map -> constr -> constr * constr list
+type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function = constr -> constr * constr list
 
-type 'a contextual_state_reduction_function = 
-    env -> 'a evar_map -> state -> state
-type 'a state_reduction_function = 'a contextual_state_reduction_function
+type contextual_state_reduction_function = 
+    env -> evar_map -> state -> state
+type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = state -> state
 
 (* Removes cast and put into applicative form *)
@@ -45,7 +45,7 @@ val whd_castapp_stack : local_stack_reduction_function
 
 (*s Reduction Function Operators *)
 
-val strong : 'a reduction_function -> 'a reduction_function
+val strong : reduction_function -> reduction_function
 val local_strong : local_reduction_function -> local_reduction_function
 val strong_prodspine : local_reduction_function -> local_reduction_function
 (*i
@@ -56,73 +56,73 @@ val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
 
 (*s Generic Optimized Reduction Function using Closures *)
 
-val clos_norm_flags : Closure.flags -> 'a reduction_function
+val clos_norm_flags : Closure.flags -> reduction_function
 (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
 val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
-val nf_betadeltaiota : 'a reduction_function
-val nf_evar : 'a evar_map -> constr -> constr
+val nf_betadeltaiota : reduction_function
+val nf_evar : evar_map -> constr -> constr
 
 (* Lazy strategy, weak head reduction *)
-val whd_evar : 'a evar_map -> constr -> constr
+val whd_evar :  evar_map -> constr -> constr
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
-val whd_betadeltaiota : 'a contextual_reduction_function
-val whd_betadeltaiota_nolet : 'a contextual_reduction_function
+val whd_betadeltaiota :  contextual_reduction_function
+val whd_betadeltaiota_nolet :  contextual_reduction_function
 val whd_betaetalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
 val whd_betaiotazeta_stack : local_stack_reduction_function
-val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function
-val whd_betadeltaiota_nolet_stack : 'a contextual_stack_reduction_function
+val whd_betadeltaiota_stack :  contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack :  contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
-val whd_betadeltaiota_state : 'a contextual_state_reduction_function
-val whd_betadeltaiota_nolet_state : 'a contextual_state_reduction_function
+val whd_betadeltaiota_state :  contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state :  contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
 
 (*s Head normal forms *)
 
-val whd_delta_stack : 'a stack_reduction_function
-val whd_delta_state : 'a state_reduction_function
-val whd_delta : 'a reduction_function
-val whd_betadelta_stack : 'a stack_reduction_function
-val whd_betadelta_state : 'a state_reduction_function
-val whd_betadelta : 'a reduction_function
-val whd_betaevar_stack : 'a stack_reduction_function
-val whd_betaevar_state : 'a state_reduction_function
-val whd_betaevar : 'a reduction_function
-val whd_betaiotaevar_stack : 'a stack_reduction_function
-val whd_betaiotaevar_state : 'a state_reduction_function
-val whd_betaiotaevar : 'a reduction_function
-val whd_betadeltaeta_stack : 'a stack_reduction_function
-val whd_betadeltaeta_state : 'a state_reduction_function
-val whd_betadeltaeta : 'a reduction_function
-val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
-val whd_betadeltaiotaeta_state : 'a state_reduction_function
-val whd_betadeltaiotaeta : 'a reduction_function
+val whd_delta_stack :  stack_reduction_function
+val whd_delta_state :  state_reduction_function
+val whd_delta :  reduction_function
+val whd_betadelta_stack :  stack_reduction_function
+val whd_betadelta_state :  state_reduction_function
+val whd_betadelta :  reduction_function
+val whd_betaevar_stack :  stack_reduction_function
+val whd_betaevar_state :  state_reduction_function
+val whd_betaevar :  reduction_function
+val whd_betaiotaevar_stack :  stack_reduction_function
+val whd_betaiotaevar_state :  state_reduction_function
+val whd_betaiotaevar :  reduction_function
+val whd_betadeltaeta_stack :  stack_reduction_function
+val whd_betadeltaeta_state :  state_reduction_function
+val whd_betadeltaeta :  reduction_function
+val whd_betadeltaiotaeta_stack :  stack_reduction_function
+val whd_betadeltaiotaeta_state :  state_reduction_function
+val whd_betadeltaiotaeta :  reduction_function
 
 val beta_applist : constr * constr list -> constr
 
-val hnf_prod_app     : env -> 'a evar_map -> constr -> constr -> constr
-val hnf_prod_appvect : env -> 'a evar_map -> constr -> constr array -> constr
-val hnf_prod_applist : env -> 'a evar_map -> constr -> constr list -> constr
-val hnf_lam_app      : env -> 'a evar_map -> constr -> constr -> constr
-val hnf_lam_appvect  : env -> 'a evar_map -> constr -> constr array -> constr
-val hnf_lam_applist  : env -> 'a evar_map -> constr -> constr list -> constr
+val hnf_prod_app     : env ->  evar_map -> constr -> constr -> constr
+val hnf_prod_appvect : env ->  evar_map -> constr -> constr array -> constr
+val hnf_prod_applist : env ->  evar_map -> constr -> constr list -> constr
+val hnf_lam_app      : env ->  evar_map -> constr -> constr -> constr
+val hnf_lam_appvect  : env ->  evar_map -> constr -> constr array -> constr
+val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
-val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr
-val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
+val splay_prod : env ->  evar_map -> constr -> (name * constr) list * constr
+val splay_arity : env ->  evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
 val decomp_n_prod : 
-  env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
+  env ->  evar_map -> int -> constr -> Sign.rel_context * constr
 val splay_prod_assum :
-  env -> 'a evar_map -> constr -> Sign.rel_context * constr
+  env ->  evar_map -> constr -> Sign.rel_context * constr
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
@@ -134,16 +134,16 @@ type 'a miota_args = {
 val reducible_mind_case : constr -> bool
 val reduce_mind_case : constr miota_args -> constr
 
-val is_arity : env -> 'a evar_map -> constr -> bool
-val is_info_type : env -> 'a evar_map -> unsafe_type_judgment -> bool
-val is_info_arity : env -> 'a evar_map -> constr -> bool
+val is_arity : env ->  evar_map -> constr -> bool
+val is_info_type : env ->  evar_map -> unsafe_type_judgment -> bool
+val is_info_arity : env ->  evar_map -> constr -> bool
 (*i Pour l'extraction
 val is_type_arity : env -> 'a evar_map -> constr -> bool
 val is_info_cast_type : env -> 'a evar_map -> constr -> bool
 val contents_of_cast_type : env -> 'a evar_map -> constr -> contents
 i*)
 
-val whd_programs : 'a reduction_function
+val whd_programs :  reduction_function
 
 (* [reduce_fix] contracts a fix redex if it is actually reducible *)
 
@@ -169,26 +169,26 @@ val pb_equal : conv_pb -> conv_pb
 val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
 val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
 
-type 'a conversion_function = 
-    env -> 'a evar_map -> constr -> constr -> constraints
+type  conversion_function = 
+    env ->  evar_map -> constr -> constr -> constraints
 
 (* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
    [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
 
-val conv : 'a conversion_function
-val conv_leq : 'a conversion_function
+val conv :  conversion_function
+val conv_leq :  conversion_function
 
 val conv_forall2 : 
-  'a conversion_function -> env -> 'a evar_map -> constr array 
+   conversion_function -> env ->  evar_map -> constr array 
     -> constr array -> constraints
 
 val conv_forall2_i : 
-  (int -> 'a conversion_function) -> env -> 'a evar_map
+  (int ->  conversion_function) -> env ->  evar_map
     -> constr array -> constr array -> constraints
 
-val is_conv : env -> 'a evar_map -> constr -> constr -> bool
-val is_conv_leq : env -> 'a evar_map -> constr -> constr -> bool
-val is_fconv : conv_pb -> env -> 'a evar_map -> constr -> constr -> bool
+val is_conv : env ->  evar_map -> constr -> constr -> bool
+val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
+val is_fconv : conv_pb -> env ->  evar_map -> constr -> constr -> bool
 
 (*s Special-Purpose Reduction Functions *)
 
@@ -201,5 +201,5 @@ val instance : (int * constr) list -> constr -> constr
 (*i
 val hnf : env -> 'a evar_map -> constr -> constr * constr list
 i*)
-val apprec : 'a state_reduction_function
+val apprec :  state_reduction_function
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index c8ef3d2e5..cec8c5f9d 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -23,14 +23,14 @@ open Environ
 
 type metamap = (int * constr) list
 
-val get_type_of : env -> 'a evar_map -> constr -> constr
-val get_sort_of : env -> 'a evar_map -> types -> sorts
-val get_sort_family_of : env -> 'a evar_map -> types -> sorts_family
+val get_type_of : env -> evar_map -> constr -> constr
+val get_sort_of : env -> evar_map -> types -> sorts
+val get_sort_family_of : env -> evar_map -> types -> sorts_family
 
-val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
+val get_type_of_with_meta : env -> evar_map -> metamap -> constr -> constr
 
 (* Makes an assumption from a constr *)
-val get_assumption_of : env -> 'a evar_map -> constr -> types
+val get_assumption_of : env -> evar_map -> constr -> types
 
 (* Makes an unsafe judgment from a constr *)
-val get_judgment_of : env -> 'a evar_map -> constr -> unsafe_judgment
+val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index fbeadc986..1b87dc712 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -22,41 +22,41 @@ open Closure
 exception Redelimination
 
 (* Red (raise Redelimination if nothing reducible) *)
-val red_product : 'a reduction_function
+val red_product : reduction_function
 
 (* Hnf *)
-val hnf_constr : 'a reduction_function
+val hnf_constr :  reduction_function
 
 (* Simpl *)
-val nf : 'a reduction_function
+val nf :  reduction_function
 
 (* Unfold *)
 val unfoldn : 
-  (int list * evaluable_global_reference) list -> 'a reduction_function
+  (int list * evaluable_global_reference) list ->  reduction_function
 
 (* Fold *)
-val fold_commands : constr list -> 'a reduction_function
+val fold_commands : constr list ->  reduction_function
 
 (* Pattern *)
-val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
+val pattern_occs : (int list * constr * constr) list ->  reduction_function
 (* Rem: Lazy strategies are defined in Reduction *)
 
 (* Call by value strategy (uses Closures) *)
-val cbv_norm_flags : Closure.flags -> 'a reduction_function
+val cbv_norm_flags : Closure.flags ->  reduction_function
   val cbv_beta : local_reduction_function
   val cbv_betaiota : local_reduction_function
-  val cbv_betadeltaiota : 'a reduction_function
-  val compute : 'a reduction_function  (* = [cbv_betadeltaiota] *)
+  val cbv_betadeltaiota :  reduction_function
+  val compute :  reduction_function  (* = [cbv_betadeltaiota] *)
 
 (* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_atomic_ind : env -> 'a evar_map -> types -> inductive * types
+val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
 
 (* [reduce_to_quantified_ind env sigma t] puts [t] in the form
    [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_quantified_ind : env -> 'a evar_map -> types -> inductive * types
+val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
 type red_expr =
   | Red of bool    (* raise Redelimination if true otherwise UserError *)
@@ -68,4 +68,4 @@ type red_expr =
   | Fold of constr list
   | Pattern of (int list * constr * constr) list
 
-val reduction_of_redexp : red_expr -> 'a reduction_function
+val reduction_of_redexp : red_expr ->  reduction_function
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 29cf0da62..e5f84bf92 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -17,11 +17,11 @@ open Evd
 (* This module provides the typing machine with existential variables
    (but without universes). *)
 
-val unsafe_machine : env -> 'a evar_map -> constr -> unsafe_judgment
+val unsafe_machine : env -> evar_map -> constr -> unsafe_judgment
 
-val type_of : env -> 'a evar_map -> constr -> constr
+val type_of : env -> evar_map -> constr -> constr
 
-val execute_type : env -> 'a evar_map -> constr -> types
+val execute_type : env -> evar_map -> constr -> types
 
-val execute_rec_type : env -> 'a evar_map -> constr -> types
+val execute_rec_type : env -> evar_map -> constr -> types