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

44 files changed, 281 insertions, 435 deletions

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index e4d4647f1b..dd6f0ef175 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -228,7 +228,7 @@ let old_sign osign sign =
 (* convertit l'arbre de preuve courant en ntree *)
 let  to_nproof sigma osign pf =
   let rec to_nproof_rec sigma osign pf =
-    let {evar_hyps=sign;evar_concl=cl;evar_info=info} = pf.goal in
+    let {evar_hyps=sign;evar_concl=cl} = pf.goal in
     let nsign = new_sign osign sign in 
     let oldsign = old_sign osign sign in 
     match pf.ref with
diff --git a/dev/db b/dev/db
index c89f2a8be8..f9a7f8d844 100644
--- a/dev/db
+++ b/dev/db
@@ -18,7 +18,6 @@ install_printer Top_printers.prj
 
 install_printer Top_printers.prgoal
 install_printer Top_printers.prsigmagoal
-install_printer Top_printers.prctxt
 install_printer Top_printers.pproof
 install_printer Top_printers.prevd
 install_printer Top_printers.prevc
diff --git a/dev/include b/dev/include
index ce923477b2..8fa4ba3744 100644
--- a/dev/include
+++ b/dev/include
@@ -18,7 +18,6 @@
 
 #install_printer  (* goal *)  prgoal;;
 #install_printer  (* sigma goal *)  prsigmagoal;;
-#install_printer  (* ctxt *)  prctxt;;
 #install_printer  (* proof *)  pproof;;
 #install_printer  (* global_constraints *)  prevd;;
 #install_printer  (* readable_constraints *)  prevc;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d3dbb6b51d..9a8670aeb9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -63,8 +63,6 @@ let prgls gls = pP(pr_gls gls)
 
 let prglls glls = pP(pr_glls glls)
 
-let prctxt ctxt = pP(pr_ctxt ctxt)
-
 let pproof p = pP(print_proof Evd.empty empty_named_context p)
 
 let prevd evd = pP(pr_decls evd)
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 31d96145a5..c850bdf43e 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -24,18 +24,18 @@ open Pattern
 val constrIn : constr -> Coqast.t
 val constrOut : Coqast.t -> constr
 
-val interp_rawconstr     : 'a evar_map -> env -> Coqast.t -> rawconstr
-val interp_constr        : 'a evar_map -> env -> Coqast.t -> constr
-val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
-val interp_type          : 'a evar_map -> env -> Coqast.t -> types
+val interp_rawconstr     : evar_map -> env -> Coqast.t -> rawconstr
+val interp_constr        : evar_map -> env -> Coqast.t -> constr
+val interp_casted_constr : evar_map -> env -> Coqast.t -> constr -> constr
+val interp_type          : evar_map -> env -> Coqast.t -> types
 val interp_sort          : Coqast.t -> sorts
 
 val interp_elimination_sort : Coqast.t -> sorts_family
 
 val interp_openconstr    :
-  'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr
+  evar_map -> env -> Coqast.t -> (existential * constr) list * constr
 val interp_casted_openconstr    :
-  'a evar_map -> env -> Coqast.t -> constr ->
+  evar_map -> env -> Coqast.t -> constr ->
     (existential * constr) list * constr
 
 (* [interp_type_with_implicits] extends [interp_type] by allowing
@@ -43,34 +43,34 @@ val interp_casted_openconstr    :
    argument associates a list of implicit positions to identifiers
    declared in the rel_context of [env] *)
 val interp_type_with_implicits : 
-  'a evar_map -> env -> 
+  evar_map -> env -> 
    (identifier * Impargs.implicits_list) list -> Coqast.t -> types
 
-val judgment_of_rawconstr : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+val judgment_of_rawconstr : evar_map -> env -> Coqast.t -> unsafe_judgment
 val type_judgment_of_rawconstr :
-  'a evar_map -> env -> Coqast.t -> unsafe_type_judgment
+  evar_map -> env -> Coqast.t -> unsafe_type_judgment
 
 (*Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it*)
 val interp_constr_gen     :
-  'a evar_map -> env -> (identifier * constr) list ->
+  evar_map -> env -> (identifier * constr) list ->
     (int * constr) list -> Coqast.t -> constr option -> constr
 
 (*Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it, and turning unresolved evar into metas*)
 val interp_openconstr_gen     :
-  'a evar_map -> env -> (identifier * constr) list ->
+  evar_map -> env -> (identifier * constr) list ->
     (int * constr) list -> Coqast.t -> constr option
       -> (existential * constr) list * constr
 
 (*Interprets constr patterns according to a list of instantiations
   (variables)*)
 val interp_constrpattern_gen :
-  'a evar_map -> env -> (identifier * constr) list -> Coqast.t ->
+  evar_map -> env -> (identifier * constr) list -> Coqast.t ->
     int list * constr_pattern
 
 val interp_constrpattern : 
-  'a evar_map -> env -> Coqast.t -> int list * constr_pattern
+  evar_map -> env -> Coqast.t -> int list * constr_pattern
 
 (*s Globalization of AST quotations (mainly used to get statically
     bound idents in grammar or pretty-printing rules) *)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index f8ea1ba1d8..f106d16d6f 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -35,7 +35,7 @@ val print_sec_context_typ : Nametab.qualid -> std_ppcmds
 val print_judgment : env -> unsafe_judgment -> std_ppcmds
 val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
-  'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
+  reduction_function -> env -> unsafe_judgment -> std_ppcmds
 (* This function is exported for the graphical user-interface pcoq *)
 val build_inductive : section_path -> int ->
   global_reference * rel_context * types * identifier array * types array
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1ecb4ce2dc..7b7ef647d6 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 3126198f9a..193882ba0f 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 eaeb25bc0e..b8817ae0ee 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 1c07a7ed34..4ca3ba9875 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 06a866f482..24830b30ac 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 533292ec71..d4a341d1ba 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 01a2437b28..66e48664a9 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 a80f21b521..ee99bfb4ba 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 f6192c7e50..f6a2bb43ac 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 7e6dd8fa1b..e28331848c 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 7ca5b8b1bb..2174bf0e96 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 4f4184769a..e66471bb5d 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 4a477b8e5a..cc36b260a8 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 11bf5b5312..5d04c50479 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 bf48e305fe..91a8da2c77 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 a34c47c5a4..410f8aa08b 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 20c9910326..8bd3ab4899 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 c8ef3d2e5b..cec8c5f9dd 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 fbeadc9860..1b87dc7124 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 29cf0da627..e5f84bf923 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
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 65307debea..b15abb775f 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -129,5 +129,5 @@ val pr_clenv : 'a clausenv -> Pp.std_ppcmds
 (* [abstract_list_all env sigma t c l]                     *)
 (* abstracts the terms in l over c to get a term of type t *)
 val abstract_list_all :
-  Environ.env -> 'a Evd.evar_map -> constr -> constr -> constr list -> constr
+  Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index a4fb3fe9b2..fe809b6244 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -32,7 +32,7 @@ type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
 type w_tactic = walking_constraints -> walking_constraints
 
 
-let local_Constraints lc gs = refiner (Local_constraints lc) gs
+let local_Constraints lc gs = refiner Change_evars gs
 
 let startWalk gls =
   let evc = project_with_focus gls in
@@ -40,11 +40,11 @@ let startWalk gls =
   (wc,
    (fun wc' gls' ->
       if not !Options.debug or (ids_eq wc wc' & gls.it = gls'.it) then
-        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then
+(*        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*)
           tclIDTAC {it=gls'.it; sigma = get_gc (ids_it wc')}
-        else
+(*        else
           (local_Constraints (get_focus (ids_it wc'))
-             {it=gls'.it; sigma = get_gc (ids_it wc')})
+             {it=gls'.it; sigma = get_gc (ids_it wc')})*)
       else error "Walking"))
 
 let walking_THEN wt rt gls =
@@ -58,17 +58,10 @@ let extract_decl sp evc =
   let evdmap = (ts_it evc).decls in
   let evd = Evd.map evdmap sp in 
   (ts_mk { hyps = evd.evar_hyps;
-           focus = get_lc evd;
            decls = Evd.rmv evdmap sp })
 
 let restore_decl sp evd evc =
-  let newctxt = { lc = (ts_it evc).focus;
-                  pgm = (get_pgm evd) } in
-  let newgoal = { evar_hyps = evd.evar_hyps; 
-		  evar_concl = evd.evar_concl;
-		  evar_body = evd.evar_body;
-                  evar_info = Some newctxt } in
-  (rc_add evc (sp,newgoal))
+  (rc_add evc (sp,evd))
 
 
 (* [w_Focusing sp wt wc]
@@ -82,8 +75,7 @@ let restore_decl sp evd evc =
 
 let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
                        (wc : walking_constraints) =
-  let focus = (ts_it (ids_it wc)).focus
-  and hyps  = (ts_it (ids_it wc)).hyps
+  let hyps  = (ts_it (ids_it wc)).hyps
   and evd   = Evd.map (ts_it (ids_it wc)).decls sp in
   let (wc' : walking_constraints) = ids_mod (extract_decl sp) wc in
   let (wc'',rslt) = wt wc' in 
@@ -96,15 +88,13 @@ let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
       (ids_mod
          (ts_mod (fun evc ->
                     { hyps = hyps;
-                      focus = focus;
                       decls = evc.decls }))
          wc''')
       
 let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
-               { focus = evr.focus;
-		 hyps = Sign.add_named_decl (id,None,t) evr.hyps;
+	       { hyps = Sign.add_named_decl (id,None,t) evr.hyps;
 		 decls = evr.decls })
             (ids_it wc))
 
@@ -135,25 +125,10 @@ let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
 
 let w_Declare sp ty (wc : walking_constraints) =
   let _ = w_type_of wc ty in (* Utile ?? *)
-  let access  = get_focus (ids_it wc)
-  and sign = get_hyps (ids_it wc) in
-  let newdecl = mk_goal (mt_ctxt access) sign ty in 
+  let sign = get_hyps (ids_it wc) in
+  let newdecl = mk_goal sign ty in 
   ((ids_mod (fun evc -> (rc_add evc (sp,newdecl))) wc): walking_constraints)
 
-let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
-
-let evars_of sigma constr = 
-  let rec filtrec acc c =
-    match kind_of_term c with
-    | Evar (ev, cl) ->
-	if Evd.in_dom (ts_it sigma).decls ev then
-	  Intset.add ev (Array.fold_left filtrec acc cl)
-	else
-	  Array.fold_left filtrec acc cl
-    | _ -> fold_constr filtrec acc c
-  in 
-  filtrec Intset.empty constr
-
 let w_Define sp c wc =
   let spdecl = Evd.map (w_Underlying wc) sp in
   let cty = 
@@ -164,10 +139,8 @@ let w_Define sp c wc =
   in 
   match spdecl.evar_body with
     | Evar_empty ->
-    	let access = evars_of (ids_it wc) c in
     	let spdecl' = { evar_hyps = spdecl.evar_hyps;
                        	evar_concl = spdecl.evar_concl;
-                       	evar_info = Some (mt_ctxt access);
                        	evar_body = Evar_defined c }
     	in 
 	(ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 88071b3af2..13a4a5e410 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -53,7 +53,6 @@ val w_Focusing_THEN :
   evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
 
 val w_Declare    : evar -> types -> w_tactic
-val w_Declare_At : evar -> evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
 val w_Underlying : walking_constraints -> enamed_declarations
@@ -74,7 +73,5 @@ val w_const_value       : walking_constraints -> constant -> constr
 val w_defined_const     : walking_constraints -> constant -> bool
 val w_defined_evar      : walking_constraints -> existential_key -> bool
 
-val evars_of     : readable_constraints -> constr -> local_constraints
-
 val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
 val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ed13b9c253..cdb45ccedc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -96,8 +96,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | Meta _ ->
 	if occur_meta conclty then
           raise (RefinerError (OccurMetaGoal conclty));
-	let ctxt = out_some goal.evar_info in 
-	(mk_goal ctxt hyps (nf_betaiota conclty))::goalacc, conclty
+	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
     | Cast (t,ty) ->
 	let _ = type_of env sigma ty in
@@ -136,8 +135,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
-	let ctxt = out_some goal.evar_info in  
-	(mk_goal ctxt hyps (nf_betaiota ty))::goalacc,ty
+	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
 
     | App (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
@@ -373,7 +371,6 @@ let prim_refiner r sigma goal =
   let env = evar_env goal in
   let sign = goal.evar_hyps in
   let cl = goal.evar_concl in
-  let info = out_some goal.evar_info in
   match r with
     | { name = Intro; newids = [id] } ->
     	if !check && mem_named_context id sign then
@@ -381,13 +378,13 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sg = mk_goal info (add_named_decl (id,None,c1) sign)
+	       let sg = mk_goal (add_named_decl (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
 	       [sg]
 	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
-		 mk_goal info (add_named_decl (id,Some c1,t1) sign)
+		 mk_goal (add_named_decl (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -401,12 +398,12 @@ let prim_refiner r sigma goal =
 	   | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = insert_after_hyp sign whereid (id,None,c1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sign' = insert_after_hyp sign whereid (id,Some c1,t1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -417,12 +414,12 @@ let prim_refiner r sigma goal =
            | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,None,c1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
            | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,Some c1,t1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -430,8 +427,8 @@ let prim_refiner r sigma goal =
 	
     | { name = Cut b; terms = [t]; newids = [id] } ->
         if occur_meta t then error_use_instantiate();
-        let sg1 = mk_goal info sign (nf_betaiota t) in
-        let sg2 = mk_goal info (add_named_decl (id,None,t) sign) cl in
+        let sg1 = mk_goal sign (nf_betaiota t) in
+        let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in
         if b then [sg1;sg2] else [sg2;sg1]  
 
     | { name = FixRule; hypspecs = []; terms = []; 
@@ -451,7 +448,7 @@ let prim_refiner r sigma goal =
      	check_ind n cl;
 	if !check && mem_named_context f sign then
 	  error ("The name "^(string_of_id f)^" is already used");
-        let sg = mk_goal info (add_named_decl (f,None,cl) sign) cl in
+        let sg = mk_goal (add_named_decl (f,None,cl) sign) cl in
         [sg]
     
     | { name = FixRule; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -479,7 +476,7 @@ let prim_refiner r sigma goal =
 		error "name already used in the environment";
 	      mk_sign (add_named_decl (f,None,ar) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
-	      List.map (mk_goal info sign) (cl::lar)
+	      List.map (mk_goal sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
 	in 
 	mk_sign sign (cl::lar,lf,ln)
@@ -505,7 +502,7 @@ let prim_refiner r sigma goal =
               with
               |	Not_found ->
                   mk_sign (add_named_decl (f,None,ar) sign) (lar',lf'))
-	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
+	  | ([],[]) -> List.map (mk_goal sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
 	mk_sign sign (cl::lar,lf)
@@ -520,19 +517,19 @@ let prim_refiner r sigma goal =
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sigma cl' in
 	if is_conv_leq env sigma cl' cl then
-          let sg = mk_goal info sign cl' in
+          let sg = mk_goal sign cl' in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
 
     | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } ->
-	[mk_goal info (convert_hyp sign sigma id ty) cl]
+	[mk_goal (convert_hyp sign sigma id ty) cl]
 
     | { name = Convert_defbody; hypspecs = [id]; terms = [c] } ->
-	[mk_goal info (convert_def true sign sigma id c) cl]
+	[mk_goal (convert_def true sign sigma id c) cl]
 
     | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } ->
-	[mk_goal info (convert_def false sign sigma id ty) cl]
+	[mk_goal (convert_def false sign sigma id ty) cl]
 
     | { name = Thin; hypspecs = ids } ->
 	let clear_aux sign id =
@@ -541,7 +538,7 @@ let prim_refiner r sigma goal =
           remove_hyp sign id 
 	in
 	let sign' = List.fold_left clear_aux sign ids in
-     	let sg = mk_goal info sign' cl in
+     	let sg = mk_goal sign' cl in
      	[sg]
 
     | { name = ThinBody; hypspecs = ids } ->
@@ -551,7 +548,7 @@ let prim_refiner r sigma goal =
           env'
 	in
 	let sign' = named_context (List.fold_left clear_aux env ids) in
-     	let sg = mk_goal info sign' cl in
+     	let sg = mk_goal sign' cl in
      	[sg]
 
     | { name = Move withdep; hypspecs = ids } ->
@@ -560,7 +557,7 @@ let prim_refiner r sigma goal =
   	let (left,right,declfrom,toleft) = split_sign hfrom hto sign in
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
-  	[mk_goal info hyps' cl]
+  	[mk_goal hyps' cl]
 	
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 3c960b657d..ba1ca70318 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -34,7 +34,7 @@ val without_check : tactic -> tactic
 
 (* The primitive refiner. *)
 
-val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> evar_map -> goal -> goal list
 
 val prim_extractor :
   (identifier list -> proof_tree -> constr)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5d015dbf83..f6424df8dc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -204,7 +204,7 @@ let delete_all_proofs = init_proofs
 (*********************************************************************)
 
 let start_proof na str sign concl =
-  let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in
+  let top_goal = mk_goal sign concl in
   let ts = { 
     top_hyps = (sign,empty_named_context);
     top_goal = top_goal;
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 3003f20c6c..c6a1df1d92 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -27,27 +27,11 @@ let is_bind = function
   | Bindings _ -> true
   | _ -> false
 
-let lc_toList lc = Intset.elements lc
-
 (* Functions on goals *)
 
-let mk_goal ctxt hyps cl = 
+let mk_goal hyps cl = 
   { evar_hyps = hyps; evar_concl = cl; 
-    evar_body = Evar_empty; evar_info = Some ctxt }
-
-(* Functions on the information associated with existential variables  *)
-
-let mt_ctxt lc = { pgm = None; lc = lc }
-
-let get_ctxt gl = out_some gl.evar_info
-
-let get_pgm gl = (out_some gl.evar_info).pgm
-
-let set_pgm pgm ctxt = { ctxt with pgm = pgm }
-
-let get_lc gl = (out_some gl.evar_info).lc
-
-let set_lc lc ctxt = { ctxt with lc = lc }
+    evar_body = Evar_empty}
 
 (* Functions on proof trees *)
 
@@ -96,7 +80,6 @@ type global_constraints  = enamed_declarations timestamped
    of existential variables and a signature. *)
 
 type evar_recordty = {
-  focus : local_constraints;
   hyps  : named_context;
   decls : enamed_declarations }
 
@@ -104,63 +87,31 @@ and readable_constraints = evar_recordty timestamped
 
 (* Functions on readable constraints *)
 			     
-let mt_evcty lc gc = 
-  ts_mk { focus = lc; hyps = empty_named_context; decls = gc }
+let mt_evcty gc = 
+  ts_mk { hyps = empty_named_context; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); hyps = gl.evar_hyps; decls = evds }
+  ts_mk { hyps = gl.evar_hyps; decls = evds }
 
 let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
 		       
 let rc_add evc (k,v) = 
   ts_mod
-    (fun evc -> { focus = (Intset.add k evc.focus);
-                  hyps  = evc.hyps;
+    (fun evc -> { hyps  = evc.hyps;
                   decls = Evd.add evc.decls k v })
     evc
 
 let get_hyps  evc = (ts_it evc).hyps
 let get_env   evc = Global.env_of_context (ts_it evc).hyps
-let get_focus evc = (ts_it evc).focus
 let get_decls evc = (ts_it evc).decls
 let get_gc    evc = (ts_mk (ts_it evc).decls)
 
 let remap evc (k,v) = 
   ts_mod
-    (fun evc -> { focus = evc.focus;
-                  hyps  = evc.hyps;
+    (fun evc -> { hyps  = evc.hyps;
                   decls = Evd.add evc.decls k v })
     evc
 
-let lc_exists f lc = Intset.fold (fun e b -> (f e) or b) lc false
-
-(* [mentions sigma sp loc] is true exactly when [loc] is defined, and [sp] is
- * on [loc]'s access list, or an evar on [loc]'s access list mentions [sp]. *)
-
-let rec mentions sigma sp loc =
-  let loc_evd = Evd.map (ts_it sigma).decls loc in 
-  match loc_evd.evar_body with 
-    | Evar_defined _ -> (Intset.mem sp (get_lc loc_evd) 
-			 or lc_exists (mentions sigma sp) (get_lc loc_evd))
-    | _ -> false
-
-(* ACCESSIBLE SIGMA SP LOC is true exactly when SP is on LOC's access list,
- * or there exists a LOC' on LOC's access list such that
- * MENTIONS SIGMA SP LOC' is true. *)
-
-let rec accessible sigma sp loc =
-  let loc_evd = Evd.map (ts_it sigma).decls loc in 
-  lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd)
-
-
-(* [ctxt_access sigma sp] is true when SIGMA is accessing a current
- * accessibility list ACCL, and SP is either on ACCL, or is mentioned
- * in the body of one of the ACCL. *)
-
-let ctxt_access sigma sp =
-  lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus
-
-
 let pf_lookup_name_as_renamed hyps ccl s =
   Detyping.lookup_name_as_renamed hyps ccl s
 
@@ -235,41 +186,27 @@ let pr_subgoal n =
   in 
   prrec n
 
-let pr_pgm ctxt = match ctxt.pgm with
-  | None -> [< >]
-  | Some pgm -> let ppgm = fprterm pgm in [< 'sTR"Realizer " ; ppgm >]
-					    
-let pr_ctxt ctxt =
-  let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >]
-
 let pr_seq evd = 
   let env = evar_env evd
   and cl = evd.evar_concl
-  and info = match evd.evar_info with 
-    | Some i -> i 
-    | None -> anomaly "pr_seq : info = None"
   in
-  let pc = pr_ctxt info in
   let pdcl = pr_named_context_of env in
   let pcl = prterm_env_at_top env cl in
-  hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
+  hOV 0 [< pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
 
 let prgl gl =
-  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
   let pgl = pr_seq gl in
-  [< 'sTR"[[" ; plc; 'sTR"]" ; pgl ; 'sTR"]" ; 'sPC >]
+  [< 'sTR"[" ; pgl ; 'sTR"]" ; 'sPC >]
 
 let pr_evgl gl =
-  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
   let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in
   let pc = prterm gl.evar_concl in
-  hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
+  hOV 0 [< 'sTR"[" ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
 let pr_evgl_sign gl = 
-  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
   let ps = pr_named_context_of (evar_env gl) in
   let pc = prterm gl.evar_concl in
-  hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
+  hOV 0 [< 'sTR"[" ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
 (*  evd.evgoal.lc seems to be printed twice *)
 let pr_decl evd =
@@ -290,13 +227,11 @@ let pr_evd evd =
     
 let pr_decls decls = pr_evd (ts_it decls)
 		       
-let pr_focus accl = pr_idl (List.map id_of_existential (lc_toList accl))
-
 let pr_evc evc =
   let stamp = ts_stamp evc in
   let evc   = ts_it evc in
   let pe = pr_evd evc.decls in
-  [< 'sTR"#" ; 'iNT stamp ; 'sTR"[" ; pr_focus evc.focus ; 'sTR"]=" ; pe >]
+  [< 'sTR"#" ; 'iNT stamp ; 'sTR"]=" ; pe >]
 
 let pr_evars = 
   prlist_with_sep pr_fnl
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index d579190b38..00f51fcca0 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -22,14 +22,7 @@ open Proof_type
 (* This module declares readable constraints, and a few utilities on
    constraints and proof trees *)
 
-val mk_goal : ctxtty -> named_context -> constr -> goal
-
-val mt_ctxt    : local_constraints -> ctxtty
-val get_ctxt   : goal -> ctxtty
-val get_pgm    : goal -> constr option
-val set_pgm    : constr option -> ctxtty -> ctxtty
-val get_lc     : goal -> local_constraints
-val set_lc     : local_constraints -> ctxtty -> ctxtty
+val mk_goal : named_context -> constr -> goal
 
 val rule_of_proof     : proof_tree -> rule
 val ref_of_proof      : proof_tree -> (rule * proof_tree list)
@@ -51,7 +44,6 @@ type global_constraints = enamed_declarations timestamped
     of existential variables and a signature. *)
 
 type evar_recordty = {
-  focus : local_constraints;
   hyps  : named_context;
   decls : enamed_declarations }
 
@@ -61,11 +53,9 @@ val rc_of_gc  : global_constraints -> goal -> readable_constraints
 val rc_add    : readable_constraints -> int * goal -> readable_constraints
 val get_hyps  : readable_constraints -> named_context
 val get_env   : readable_constraints -> env
-val get_focus : readable_constraints -> local_constraints
 val get_decls : readable_constraints -> enamed_declarations
 val get_gc    : readable_constraints -> global_constraints
 val remap     : readable_constraints -> int * goal -> readable_constraints
-val ctxt_access : readable_constraints -> int -> bool
 
 val pf_lookup_name_as_renamed : 
   named_context -> constr -> identifier -> int option
@@ -88,8 +78,6 @@ val pr_evc       : readable_constraints -> std_ppcmds
 
 val prgl         : goal -> std_ppcmds
 val pr_seq       : goal -> std_ppcmds
-val pr_focus     : local_constraints -> std_ppcmds
-val pr_ctxt      : ctxtty -> std_ppcmds
 val pr_evars     : (int * goal) list -> std_ppcmds
 val pr_evars_int : int -> (int * goal) list -> std_ppcmds
 val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 1109a5837d..c866d85ed5 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -57,11 +57,7 @@ type prim_rule = {
 
 type local_constraints = Intset.t
 
-type ctxtty = {
-  pgm    : constr option;
-  lc     : local_constraints } 
-
-type enamed_declarations = ctxtty evar_map
+type enamed_declarations = evar_map
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
@@ -88,10 +84,9 @@ type proof_tree = {
 and rule =
   | Prim of prim_rule
   | Tactic of tactic_expression
-  | Context of ctxtty
-  | Local_constraints of local_constraints
+  | Change_evars
 
-and goal = ctxtty evar_info
+and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index bf7162aa3a..3d972da3f9 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -60,11 +60,7 @@ type prim_rule = {
 
 type local_constraints = Intset.t
 
-type ctxtty = {
-  pgm    : constr option;
-  lc     : local_constraints } 
-
-type enamed_declarations = ctxtty evar_map
+type enamed_declarations = evar_map
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
@@ -120,10 +116,9 @@ type proof_tree = {
 and rule =
   | Prim of prim_rule
   | Tactic of tactic_expression
-  | Context of ctxtty
-  | Local_constraints of local_constraints
+  | Change_evars
 
-and goal = ctxtty evar_info
+and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 820c6eaff6..921238d459 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -58,8 +58,7 @@ let norm_goal sigma gl =
       (fun (d,b,ty) sign ->
         add_named_decl (d, option_app red_fun b, red_fun ty) sign)
       empty_named_context gl.evar_hyps;
-    evar_body = gl.evar_body;
-    evar_info = gl.evar_info }
+    evar_body = gl.evar_body}
 
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -184,27 +183,13 @@ let refiner = function
               subproof = Some hidden_proof;
               ref = Some(r,spfl) }))
       
-  | (Context ctxt) as r ->
-      (fun goal_sigma ->
-         let gl = goal_sigma.it in
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
-         ({it=[sg];sigma=goal_sigma.sigma},
-          (fun spfl -> 
-	     assert (check_subproof_connection [sg] spfl);
-             { status = (List.hd spfl).status;
-               goal = gl;
-               subproof = None;
-               ref = Some(r,spfl) })))
-
    (* [Local_constraints lc] makes the local constraints be [lc] and
       normalizes evars *)
 
-  | (Local_constraints lc) as r ->
+  | Change_evars as r ->
       (fun goal_sigma ->
          let gl = goal_sigma.it in
-         let ctxt = set_lc lc (out_some gl.evar_info) in 
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
-	 let sgl = [norm_goal (ts_it goal_sigma.sigma) sg] in
+	 let sgl = [norm_goal (ts_it goal_sigma.sigma) gl] in
 	 ({it=sgl;sigma=goal_sigma.sigma},
           (fun spfl -> 
 	    assert (check_subproof_connection sgl spfl);
@@ -213,9 +198,8 @@ let refiner = function
                subproof = None;
                ref = Some(r,spfl) })))
 
-let context ctxt = refiner (Context ctxt)
 let vernac_tactic texp = refiner (Tactic texp)
-let norm_evar_tac gl = refiner (Local_constraints (get_lc gl.it)) gl
+let norm_evar_tac gl = refiner Change_evars gl
 
 (* [rc_of_pfsigma : proof sigma -> readable_constraints] *)
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
@@ -241,9 +225,7 @@ let extract_open_proof sigma pf =
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
 	  
-    | {ref=Some(Context ctxt,[pf])} -> (proof_extractor vl) pf
-	  
-    | {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
+    | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
 	  
     | {ref=None;goal=goal} ->
 	let visible_rels =
@@ -390,8 +372,7 @@ let rec tclTHENLIST = function
 (* various progress criterions *)
 let same_goal gl subgoal = 
   (hypotheses subgoal) = (hypotheses gl) &
-  eq_constr (conclusion subgoal) (conclusion gl) &
-  (subgoal.evar_info = gl.evar_info)
+  eq_constr (conclusion subgoal) (conclusion gl)
 
 
 let weak_progress gls ptree =
@@ -801,8 +782,7 @@ let pr_tactic (s,l) =
 let pr_rule = function
   | Prim r -> pr_prim_rule r
   | Tactic texp -> hOV 0 (pr_tactic texp)
-  | Context ctxt -> pr_ctxt ctxt
-  | Local_constraints lc ->
+  | Change_evars ->
       (* This is internal tactic and cannot be replayed at user-level *)
       (* [< 'sTR"Local constraint change" >] *)
       (* Use Idtac instead *)
@@ -823,15 +803,15 @@ let thin_sign osign sign =
 
 let rec print_proof sigma osign pf =
   let {evar_hyps=hyps; evar_concl=cl; 
-       evar_info=info; evar_body=body} = pf.goal in
+       evar_body=body} = pf.goal in
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
 	hOV 0 [< pr_seq {evar_hyps=hyps'; evar_concl=cl;
-			 evar_info=info; evar_body=body} >]
+			 evar_body=body} >]
     | Some(r,spfl) ->
     	hOV 0 [< hOV 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl;
-				evar_info=info; evar_body=body});
+				evar_body=body});
 		 'sPC ; 'sTR" BY ";
 		 hOV 0 [< pr_rule r >]; 'fNL ;
 		 'sTR"  ";
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index dd85f004ae..290c7debcc 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -34,7 +34,6 @@ val overwriting_add_tactic : string -> (tactic_arg list -> tactic) -> unit
 val lookup_tactic          : string -> (tactic_arg list) -> tactic
 
 val refiner : rule -> tactic
-val context : ctxtty -> tactic
 val vernac_tactic : tactic_expression -> tactic
 val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e5ccf6d326..f4766963f9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -71,8 +71,6 @@ let pf_get_hyp_typ gls id =
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
-let pf_ctxt gls      = get_ctxt (sig_it gls)
-
 let pf_interp_constr gls c =
   let evc = project gls in 
   Astterm.interp_constr evc (pf_env gls) c
@@ -287,7 +285,6 @@ let rename_bound_var_goal gls =
 (***************************************)
 
 let vernac_tactic = vernac_tactic
-let context       = context
 
 let add_tactic = Refiner.add_tactic
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index c81748a283..48dcb23689 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -45,7 +45,6 @@ val pf_hyps_types         : goal sigma -> (identifier * constr) list
 val pf_nth_hyp_id         : goal sigma -> int -> identifier
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> identifier list
-val pf_ctxt               : goal sigma -> ctxtty
 val pf_global             : goal sigma -> identifier -> constr
 val pf_parse_const        : goal sigma -> string -> constr
 val pf_type_of            : goal sigma -> constr -> constr
@@ -151,8 +150,6 @@ val tclINFO          : tactic -> tactic
 
 val unTAC         : tactic -> goal sigma -> proof_tree sigma
 val vernac_tactic : tactic_expression -> tactic
-val context       : ctxtty -> tactic
-
 
 (*s The most primitive tactics. *)
 
@@ -246,7 +243,7 @@ val hide_cbindll_tactic :
 open Pp
 (*i*)
 
-val pr_com    : 'a Evd.evar_map -> goal -> Coqast.t -> std_ppcmds
+val pr_com    : Evd.evar_map -> goal -> Coqast.t -> std_ppcmds
 val pr_gls    : goal sigma -> std_ppcmds
 val pr_glls   : goal list sigma -> std_ppcmds
 val pr_tactic : tactic_expression -> std_ppcmds
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 504cb8ba93..20f770b833 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -76,7 +76,7 @@ val make_exact_entry :
    [cty] is the type of [hc]. *)
 
 val make_apply_entry :
-  env -> 'a evar_map -> bool * bool -> identifier -> constr * constr
+  env -> evar_map -> bool * bool -> identifier -> constr * constr
       -> constr_label * pri_auto_tactic
 
 (* A constr which is Hint'ed will be:
@@ -87,7 +87,7 @@ val make_apply_entry :
        has missing arguments. *)
 
 val make_resolves :
-  env -> 'a evar_map -> identifier -> bool * bool -> constr * constr -> 
+  env -> evar_map -> identifier -> bool * bool -> constr * constr -> 
     (constr_label * pri_auto_tactic) list
 
 (* [make_resolve_hyp hname htyp].
@@ -96,7 +96,7 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp : 
-  env -> 'a evar_map -> named_declaration ->
+  env -> evar_map -> named_declaration ->
       (constr_label * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index b7ec9eb591..cfda6dc345 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -87,7 +87,7 @@ val dEq : clause -> tactic
 val dEqThen : (int -> tactic) -> clause -> tactic
 
 val make_iterated_tuple : 
-  env -> 'a evar_map -> (constr * constr) -> (constr * constr) 
+  env -> evar_map -> (constr * constr) -> (constr * constr) 
     -> constr * constr * constr
 
 val subst : constr -> clause -> tactic
@@ -95,7 +95,7 @@ val hypSubst : identifier -> clause -> tactic
 val revSubst : constr -> clause -> tactic
 val revHypSubst : identifier -> clause -> tactic
 
-val discriminable : env -> 'a evar_map -> constr -> constr -> bool
+val discriminable : env -> evar_map -> constr -> constr -> bool
 
 (***************)
 (* AutoRewrite *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index ab0590a714..2fa36bf20c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -212,7 +212,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     [< 'sTR"Computed inversion goal was not closed in initial signature" >];
   *)
   let invSign = named_context invEnv in
-  let pfs = mk_pftreestate (mk_goal (mt_ctxt Intset.empty) invSign invGoal) in
+  let pfs = mk_pftreestate (mk_goal invSign invGoal) in
   let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
   let global_named_context = Global.named_context () in
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 8f9cad9a9d..cd88cc1b5b 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -36,8 +36,8 @@ type wc = walking_constraints
 
 val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
 
-val add_prod_rel : 'a evar_map -> constr * env -> constr * env
-val add_prods_rel : 'a evar_map -> constr * env -> constr * env
+val add_prod_rel : evar_map -> constr * env -> constr * env
+val add_prods_rel : evar_map -> constr * env -> constr * env
 
 (*i**
 val add_prod_sign :