deplacements des var. ex. hors du noyau

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

18 files changed, 249 insertions, 584 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 49be8a1a5d..a7ee12c3e4 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -10,7 +10,6 @@ open Inductive
 open Environ
 open Instantiate
 open Univ
-open Evd
 
 
 let stats = ref false
@@ -136,7 +135,7 @@ let red_under (md,r) rk =
 type ('a, 'b) infos = {
   i_flags : flags;
   i_repr : ('a, 'b) infos -> constr -> 'a;
-  i_env : 'b unsafe_env;
+  i_env : unsafe_env;
   i_tab : (constr, 'a) Hashtbl.t }
 
 let const_value_cache info c =
@@ -150,8 +149,8 @@ let const_value_cache info c =
           Some v
       | None -> None
 
-let infos_under { i_flags = flg; i_repr = rfun; i_env = sigma; i_tab = tab } =
-  { i_flags = flags_under flg; i_repr = rfun; i_env = sigma; i_tab = tab }
+let infos_under { i_flags = flg; i_repr = rfun; i_env = env; i_tab = tab } =
+  { i_flags = flags_under flg; i_repr = rfun; i_env = env; i_tab = tab }
 
 
 (**** Call by value reduction ****)
@@ -465,10 +464,10 @@ and cbv_norm_value info = function (* reduction under binders *)
 type 'a cbv_infos = (cbv_value, 'a) infos
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs sigma =
+let create_cbv_infos flgs env =
   { i_flags = flgs;
     i_repr = (fun old_info c -> cbv_stack_term old_info TOP ESID c);
-    i_env = sigma;
+    i_env = env;
     i_tab = Hashtbl.create 17 }
 
 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 62caafe557..ea7defa201 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,6 @@ open Pp
 open Names
 open Generic
 open Term
-open Evd
 open Environ
 (*i*)
 
@@ -83,7 +82,7 @@ val fixp_reducible :
 
 (* normalization of a constr: the two functions to know... *)
 type 'a cbv_infos
-val create_cbv_infos : flags -> 'a unsafe_env -> 'a cbv_infos
+val create_cbv_infos : flags -> unsafe_env -> 'a cbv_infos
 val cbv_norm : 'a cbv_infos -> constr -> constr
 
 (* recursive functions... *)
@@ -159,8 +158,8 @@ type case_status =
 
 (* Constant cache *)
 type 'a clos_infos
-val create_clos_infos : flags -> 'a unsafe_env -> 'a clos_infos
-val clos_infos_env : 'a clos_infos -> 'a unsafe_env
+val create_clos_infos : flags -> unsafe_env -> 'a clos_infos
+val clos_infos_env : 'a clos_infos -> unsafe_env
 
 (* Reduction function *)
 val norm_val : 'a clos_infos -> fconstr -> constr
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e54de389c7..c0f49ee1ef 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -9,7 +9,6 @@ open Sign
 open Univ
 open Generic
 open Term
-open Evd
 open Constant
 open Inductive
 open Abstraction
@@ -27,11 +26,9 @@ type globals = {
   env_locals : (global * section_path) list;
   env_imports : import list }
 
-type 'a unsafe_env = {
+type unsafe_env = {
   env_context : context;
   env_globals : globals;
-  env_sigma : 'a evar_map;
-  env_metamap : (int * constr) list;
   env_universes : universes }
 
 let empty_env = { 
@@ -42,13 +39,9 @@ let empty_env = {
     env_abstractions = Spmap.empty;
     env_locals = [];
     env_imports = [] };
-  env_sigma = mt_evd;
-  env_metamap = [];
   env_universes = initial_universes }
 
 let universes env = env.env_universes
-let metamap env = env.env_metamap
-let evar_map env = env.env_sigma
 let context env = env.env_context
 
 (* Construction functions. *)
@@ -122,9 +115,6 @@ let lookup_mind_specif i env =
 	  mis_mip = mind_nth_type_packet mib tyi }
     | _ -> invalid_arg "lookup_mind_specif"
 
-let lookup_meta n env =
-  List.assoc n env.env_metamap
-
 let lookup_abst sp env =
   Spmap.find sp env.env_globals.env_abstractions
 
@@ -204,32 +194,6 @@ let defined_constant env = function
       Constant.is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
 
-(* A constant is an existential if its name has the existential id prefix *)
-let existential_id_prefix = "?"
-
-let is_existential_id id =
-  atompart_of_id id = existential_id_prefix
-
-let is_existential_oper = function
-  | Const sp -> is_existential_id (basename sp)
-  | _ -> false
-
-let is_existential = function
-  | DOPN (oper, _) -> is_existential_oper oper
-  | _ -> false
-
-let defined_existential env = function
-  | DOPN (Const sp, _) -> 
-      Evd.is_defined env.env_sigma sp
-  | _ -> invalid_arg "defined_existential"
-
-let defined_const env c =
-  (defined_constant env c) || 
-  ((is_existential c) && (defined_existential env c))
-
-let translucent_const env c =
-  (is_existential c) && (defined_existential env c)
-
 (* A const is opaque if it is a non-defined existential or
    a non-existential opaque constant *)
 
@@ -238,18 +202,10 @@ let opaque_constant env = function
       Constant.is_opaque (lookup_constant sp env)
   | _ -> invalid_arg "opaque_constant"
 
-let opaque_const env = function
-  | DOPN(Const sp,_) as k ->
-      if is_existential k then
-        not (defined_existential env k)
-      else 
-	opaque_constant env k
-  | _ -> invalid_arg "opaque_const"
-
 (* A const is evaluable if it is defined and not opaque *)
-let evaluable_const env k =
+let evaluable_constant env k =
   try 
-    defined_const env k && not (opaque_const env k)
+    defined_constant env k && not (opaque_constant env k)
   with Not_found -> 
     false
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4d979f0dc7..c611fea0b8 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -7,7 +7,6 @@ open Term
 open Constant
 open Inductive
 open Abstraction
-open Evd
 open Univ
 open Sign
 (*i*)
@@ -17,56 +16,50 @@ open Sign
    informations added in environments, and that is what we speak here
    of ``unsafe'' environments. *)
 
-type 'a unsafe_env
+type unsafe_env
 
-val empty_env : 'a unsafe_env
+val empty_env : unsafe_env
 
-val evar_map : 'a unsafe_env -> 'a evar_map
-val universes : 'a unsafe_env -> universes
-val metamap : 'a unsafe_env -> (int * constr) list
-val context : 'a unsafe_env -> context
+val universes : unsafe_env -> universes
+val context : unsafe_env -> context
 
-val push_var : identifier * typed_type -> 'a unsafe_env -> 'a unsafe_env
-val push_rel : name * typed_type -> 'a unsafe_env -> 'a unsafe_env
-val set_universes : universes -> 'a unsafe_env -> 'a unsafe_env
-val add_constraints : constraints -> 'a unsafe_env -> 'a unsafe_env
+val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
+val push_rel : name * typed_type -> unsafe_env -> unsafe_env
+val set_universes : universes -> unsafe_env -> unsafe_env
+val add_constraints : constraints -> unsafe_env -> unsafe_env
 val add_constant : 
-  section_path -> constant_body -> 'a unsafe_env -> 'a unsafe_env
+  section_path -> constant_body -> unsafe_env -> unsafe_env
 val add_mind : 
-  section_path -> mutual_inductive_body -> 'a unsafe_env -> 'a unsafe_env
+  section_path -> mutual_inductive_body -> unsafe_env -> unsafe_env
 val add_abstraction : 
-  section_path -> abstraction_body -> 'a unsafe_env -> 'a unsafe_env
+  section_path -> abstraction_body -> unsafe_env -> unsafe_env
 
 val new_meta : unit -> int
 
-val lookup_var : identifier -> 'a unsafe_env -> name * typed_type
-val lookup_rel : int -> 'a unsafe_env -> name * typed_type
-val lookup_constant : section_path -> 'a unsafe_env -> constant_body
-val lookup_mind : section_path -> 'a unsafe_env -> mutual_inductive_body
-val lookup_mind_specif : constr -> 'a unsafe_env -> mind_specif
-val lookup_meta : int -> 'a unsafe_env -> constr
+val lookup_var : identifier -> unsafe_env -> name * typed_type
+val lookup_rel : int -> unsafe_env -> name * typed_type
+val lookup_constant : section_path -> unsafe_env -> constant_body
+val lookup_mind : section_path -> unsafe_env -> mutual_inductive_body
+val lookup_mind_specif : constr -> unsafe_env -> mind_specif
 
-val id_of_global : 'a unsafe_env -> sorts oper -> identifier
-val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier
-val named_hd : 'a unsafe_env -> constr -> name -> name
-val prod_name : 'a unsafe_env -> name * constr * constr -> constr
+val id_of_global : unsafe_env -> sorts oper -> identifier
+val id_of_name_using_hdchar : unsafe_env -> constr -> name -> identifier
+val named_hd : unsafe_env -> constr -> name -> name
+val prod_name : unsafe_env -> name * constr * constr -> constr
 
-val translucent_abst : 'a unsafe_env -> constr -> bool
-val evaluable_abst : 'a unsafe_env -> constr -> bool
-val abst_value : 'a unsafe_env -> constr -> constr
+val translucent_abst : unsafe_env -> constr -> bool
+val evaluable_abst : unsafe_env -> constr -> bool
+val abst_value : unsafe_env -> constr -> constr
 
-val defined_const : 'a unsafe_env -> constr -> bool
-val translucent_const : 'a unsafe_env -> constr -> bool
-val evaluable_const : 'a unsafe_env -> constr -> bool
-
-val is_existential : constr -> bool
+val defined_constant : unsafe_env -> constr -> bool
+val evaluable_constant : unsafe_env -> constr -> bool
 
 (*s Modules. *)
 
 type compiled_env
 
-val export : 'a unsafe_env -> string -> compiled_env
-val import : compiled_env -> 'a unsafe_env -> 'a unsafe_env
+val export : unsafe_env -> string -> compiled_env
+val import : compiled_env -> unsafe_env -> unsafe_env
 
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
diff --git a/kernel/evd.ml b/kernel/evd.ml
deleted file mode 100644
index e5197db4e2..0000000000
--- a/kernel/evd.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-
-(* $Id$ *)
-
-open Util
-open Names
-open Term
-open Sign
-
-(* The type of mappings for existential variables *)
-
-type evar_body =
-  | EVAR_EMPTY 
-  | EVAR_DEFINED of constr
-
-type 'a evar_info = {
-  evar_concl : typed_type;           (* the type of the evar ...          *)
-  evar_hyps  : typed_type signature; (* ... under a certain signature     *)
-  evar_body  : evar_body;            (* its definition                    *) 
-  evar_info  : 'a option }           (* any other necessary information   *)
-
-type 'a evar_map = 'a evar_info Spmap.t
-
-let mt_evd = Spmap.empty
-
-let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc []
-let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc []
-let map evc k = Spmap.find k evc
-let rmv evc k = Spmap.remove k evc
-let remap evc k i = Spmap.add k i evc
-let in_dom evc k = Spmap.mem k evc
-
-let add_with_info evd sp newinfo = 
-  Spmap.add sp newinfo evd
-
-let add_noinfo evd sp sign typ = 
-  let newinfo = 
-    { evar_concl = typ;
-      evar_hyps  = sign;
-      evar_body  = EVAR_EMPTY;
-      evar_info  = None}
-  in 
-  Spmap.add sp newinfo evd
-
-let define evd sp body = 
-  let oldinfo = map evd sp in
-  let newinfo =
-    { evar_concl = oldinfo.evar_concl;
-      evar_hyps  = oldinfo.evar_hyps;
-      evar_body  = EVAR_DEFINED body;
-      evar_info  = oldinfo.evar_info} 
-  in
-  match oldinfo.evar_body with
-    | EVAR_EMPTY -> Spmap.add sp newinfo evd
-    | _ -> anomaly "cannot define an isevar twice"
-
-(* The list of non-instantiated existential declarations *)
-
-let non_instantiated sigma = 
-  let listsp = toList sigma in
-  List.fold_left 
-    (fun l ((sp,evd) as d) -> 
-       if evd.evar_body = EVAR_EMPTY then (d::l) else l)
-    [] listsp
-    
-let is_evar sigma sp = in_dom sigma sp
-
-let is_defined sigma sp =
-  let info = map sigma sp in not (info.evar_body = EVAR_EMPTY)
diff --git a/kernel/evd.mli b/kernel/evd.mli
deleted file mode 100644
index 696fcdd3b3..0000000000
--- a/kernel/evd.mli
+++ /dev/null
@@ -1,48 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Term
-open Sign
-(*i*)
-
-(* The type of mappings for existential variables.
-   The keys are section paths and the associated information is a record
-   containing the type of the evar ([concl]), the signature under which 
-   it was introduced ([hyps]), its definition ([body]) and any other 
-   possible information if necessary ([info]).
-*)
-
-type evar_body =
-  | EVAR_EMPTY 
-  | EVAR_DEFINED of constr
-
-type 'a evar_info = {
-  evar_concl : typed_type;
-  evar_hyps  : typed_type signature;
-  evar_body  : evar_body;
-  evar_info  : 'a option }
-
-type 'a evar_map
-
-val dom    : 'a evar_map -> section_path list
-val map    : 'a evar_map -> section_path -> 'a evar_info
-val rmv    : 'a evar_map -> section_path -> 'a evar_map
-val remap  : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val in_dom : 'a evar_map -> section_path -> bool
-val toList : 'a evar_map -> (section_path * 'a evar_info) list
-
-val mt_evd : 'a evar_map
-val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val add_noinfo : 
-  'a evar_map -> section_path -> typed_type signature -> typed_type 
-    -> 'a evar_map
-
-val define : 'a evar_map -> section_path -> constr -> 'a evar_map
-
-val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
-val is_evar : 'a evar_map -> section_path -> bool
-
-val is_defined : 'a evar_map -> section_path -> bool
-
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 8a200aab0a..a77cc09217 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -12,12 +12,12 @@ open Environ
 (* [mind_check_arities] checks that the types declared for all the
    inductive types are some arities. *)
 
-val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit
+val mind_check_arities : unsafe_env -> mutual_inductive_entry -> unit
 
-val sort_of_arity : 'a unsafe_env -> constr -> sorts
+val sort_of_arity : unsafe_env -> constr -> sorts
 
 val cci_inductive : 
-  'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> 
+  unsafe_env -> unsafe_env -> path_kind -> int -> bool -> 
     (identifier * typed_type * identifier list * bool * bool * constr) list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 9b4c1ae710..679789d6ce 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -9,7 +9,6 @@ open Term
 open Sign
 open Constant
 open Inductive
-open Evd
 open Environ
 
 let is_id_inst ids args =
@@ -41,7 +40,7 @@ let constant_type env k =
 let constant_value env k =
   let (sp,args) = destConst k in
   let cb = lookup_constant sp env in
-  if not cb.const_opaque & defined_const env k then
+  if not cb.const_opaque & defined_constant env k then
     match cb.const_body with
       Some { contents = Cooked body } -> 
         instantiate_constr 
@@ -53,52 +52,10 @@ let constant_value env k =
           [< 'sTR "a defined constant as no body." >]
   else failwith "opaque"
 
-
-(* existential_type gives the type of an existential *)
-let existential_type env k = 
-  let (sp,args) = destConst k in
-  let evd = Evd.map (evar_map env) sp in
-  instantiate_constr 
-    (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args)
-
-(* existential_value gives the value of a defined existential *)
-let existential_value env k =
-  let (sp,args) = destConst k in
-  if defined_const env k then
-    let evd = Evd.map (evar_map env) sp in
-    match evd.evar_body with
-      | EVAR_DEFINED c ->
- 	  instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args)
-      | _ -> anomalylabstrm "termenv__existential_value"
-            [< 'sTR"The existential variable code just registered a" ;
-               'sPC ; 'sTR"grave internal error." >]
-  else 
-    failwith "undefined existential"
-
-(* Constants or existentials. *)
-
-(* gives the value of a const *)
-let const_or_ex_value env = function
-  | DOPN (Const sp, _) as k -> 
-      if is_existential k then
-        existential_value env k
-      else 
-	constant_value env k
-  | _ -> invalid_arg "const_or_ex_value"
-
-(* gives the type of a const *)
-let const_or_ex_type env = function
-  | DOPN (Const sp, _) as k -> 
-      if is_existential k then
-	existential_type env k
-      else 
-	(constant_type env k).body
-  | _ -> invalid_arg "const_or_ex_type"
-
 let const_abst_opt_value env c =
   match c with
     | DOPN(Const sp,_) ->
-	if evaluable_const env c then Some (const_or_ex_value env c) else None
+	if evaluable_constant env c then Some (constant_value env c) else None
     | DOPN(Abst sp,_) ->
 	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 73d6de1b12..cc63b9a547 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -15,13 +15,10 @@ val instantiate_constr :
 val instantiate_type : 
   identifier list -> typed_type -> constr list -> typed_type
 
-val constant_value : 'a unsafe_env -> constr -> constr
-val constant_type : 'a unsafe_env -> constr -> typed_type
+val constant_value : unsafe_env -> constr -> constr
+val constant_type : unsafe_env -> constr -> typed_type
 
-val const_or_ex_value : 'a unsafe_env -> constr -> constr
-val const_or_ex_type : 'a unsafe_env -> constr -> constr
+val const_abst_opt_value : unsafe_env -> constr -> constr option
 
-val const_abst_opt_value : 'a unsafe_env -> constr -> constr option
-
-val mis_lc : 'a unsafe_env -> mind_specif -> constr
+val mis_lc : unsafe_env -> mind_specif -> constr
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2d19f44857..3d67e57d4e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -7,22 +7,19 @@ open Names
 open Generic
 open Term
 open Univ
-open Evd
 open Constant
 open Inductive
 open Environ
 open Instantiate
 open Closure
 
-let mt_evd = Evd.mt_evd
-
 exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = 'a unsafe_env -> constr -> constr
-type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list 
-  -> constr * constr list
+type 'a reduction_function = unsafe_env -> constr -> constr
+type 'a stack_reduction_function = 
+    unsafe_env -> constr -> constr list -> constr * constr list
 
 (*************************************)
 (*** Reduction Functions Operators ***)
@@ -101,7 +98,7 @@ let red_product env c =
     match x with
       | DOPN(AppL,cl) -> 
 	  DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl))
-      | DOPN(Const _,_) when evaluable_const env x -> const_or_ex_value env x
+      | DOPN(Const _,_) when evaluable_constant env x -> constant_value env x
       | DOPN(Abst _,_) when evaluable_abst env x -> abst_value env x 
       | DOP2(Cast,c,_) -> redrec c
       | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b))  
@@ -180,10 +177,10 @@ let subst_term_occ locs c t =
 let rec substlin env name n ol c =
   match c with
     | DOPN(Const sp,_) ->
-        if (path_of_const c)=name then
-          if (List.hd ol)=n then
-            if evaluable_const env c then 
-	      ((n+1),(List.tl ol), const_or_ex_value env c)
+        if path_of_const c = name then
+          if List.hd ol = n then
+            if evaluable_constant env c then 
+	      ((n+1),(List.tl ol), constant_value env c)
             else
               errorlabstrm "substlin"
                 [< 'sTR(string_of_path sp);
@@ -194,8 +191,8 @@ let rec substlin env name n ol c =
 	  (n,ol,c)
 
     | DOPN(Abst _,_) ->
-        if (path_of_abst c)=name then
-          if (List.hd ol)=n then 
+        if path_of_abst c = name then
+          if List.hd ol = n then 
 	    ((n+1),(List.tl ol), abst_value env c)
           else 
 	    ((n+1),ol,c)
@@ -363,8 +360,8 @@ let whd_const_stack namelist env =
     match x with
       | DOPN(Const sp,_) as c ->
 	  if List.mem sp namelist then
-            if evaluable_const env c then
-              whrec (const_or_ex_value env c) l
+            if evaluable_constant env c then
+              whrec (constant_value env c) l
             else 
 	      error "whd_const_stack"
 	  else 
@@ -391,8 +388,8 @@ let whd_delta_stack env =
   let rec whrec x l =
     match x with
       | DOPN(Const _,_) as c ->
-	  if evaluable_const env c then
-            whrec (const_or_ex_value env c) l
+	  if evaluable_constant env c then
+            whrec (constant_value env c) l
 	  else 
 	    x,l
       | (DOPN(Abst _,_)) as c ->
@@ -413,8 +410,8 @@ let whd_betadelta_stack env =
   let rec whrec x l =
     match x with
       | DOPN(Const _,_) ->
-          if evaluable_const env x then 
-	    whrec (const_or_ex_value env x) l
+          if evaluable_constant env x then 
+	    whrec (constant_value env x) l
           else 
 	    (x,l)
       | DOPN(Abst _,_) ->
@@ -439,8 +436,8 @@ let whd_betadeltat_stack env =
   let rec whrec x l =
     match x with
       | DOPN(Const _,_) ->
-          if translucent_const env x then 
-	    whrec (const_or_ex_value env x) l
+          if evaluable_constant env x then 
+	    whrec (constant_value env x) l
           else 
 	    (x,l)
       | DOPN(Abst _,_) ->
@@ -464,8 +461,8 @@ let whd_betadeltaeta_stack env =
   let rec whrec x stack =
     match x with
       | DOPN(Const _,_) ->
-          if evaluable_const env x then
-	    whrec (const_or_ex_value env x) stack
+          if evaluable_constant env x then
+	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -607,8 +604,8 @@ let whd_betadeltatiota_stack env =
   let rec whrec x stack =
     match x with
       | DOPN(Const _,_) ->
-          if translucent_const env x then
-            whrec (const_or_ex_value env x) stack
+          if evaluable_constant env x then
+            whrec (constant_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -643,8 +640,8 @@ let whd_betadeltaiota_stack env =
   let rec bdi_rec x stack =
     match x with
       | DOPN(Const _,_) ->
-          if evaluable_const env x then
-	    bdi_rec (const_or_ex_value env x) stack
+          if evaluable_constant env x then
+	    bdi_rec (constant_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -680,8 +677,8 @@ let whd_betadeltaiotaeta_stack env =
   let rec whrec x stack =
     match x with
       | DOPN(Const _,_) ->
-          if evaluable_const env x then 
-	    whrec (const_or_ex_value env x) stack
+          if evaluable_constant env x then 
+	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -742,7 +739,7 @@ let pb_equal = function
   | CONV_LEQ -> CONV
   | CONV -> CONV
 
-type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints
+type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
 
 (* Conversion utility functions *)
 
@@ -939,35 +936,6 @@ let is_conv env = test_conversion conv env
 let is_conv_leq env = test_conversion conv_leq env
 
 
-(********************************************************************)
-(*             Special-Purpose Reduction                            *)
-(********************************************************************)
-
-let whd_meta env = function
-  | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u)
-  | x -> x
-	
-(* Try to replace all metas. Does not replace metas in the metas' values
- * Differs from (strong whd_meta). *)
-let plain_instance env c = 
-  let s = metamap env in
-  let rec irec = function
-    | DOP0(Meta p) as u -> (try List.assoc p s with Not_found -> u)
-    | DOP1(oper,c)      -> DOP1(oper, irec c)
-    | DOP2(oper,c1,c2)  -> DOP2(oper, irec c1, irec c2)
-    | DOPN(oper,cl)     -> DOPN(oper, Array.map irec cl)
-    | DOPL(oper,cl)     -> DOPL(oper, List.map irec cl)
-    | DLAM(x,c)         -> DLAM(x, irec c)
-    | DLAMV(x,v)        -> DLAMV(x, Array.map irec v)
-    | u                 -> u
-  in 
-  if s = [] then c else irec c
-    
-(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
-let instance env c = 
-  let s = metamap env in
-  if s = [] then c else nf_betaiota env (plain_instance env c)
-
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -1048,8 +1016,8 @@ let special_red_case env whfun p c ci lf  =
     let (constr,cargs) = whfun c l in 
     match constr with 
       | DOPN(Const _,_) as g -> 
-          if (evaluable_const env g) then
-            let gvalue = (const_or_ex_value env g) in
+          if evaluable_constant env g then
+            let gvalue = constant_value env g in
             if reducible_mind_case  gvalue then
               reduce_mind_case_use_function env g
                 {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
@@ -1335,51 +1303,6 @@ let poly_args env t =
     | DOP2(Prod,a,DLAM(_,b)) -> aux 1 b
     | _ -> []
 
-(* Expanding existential variables (trad.ml, progmach.ml) *)
-(* 1- whd_ise fails if an existential is undefined *)
-let rec whd_ise env = function
-  | DOPN(Const sp,_) as k ->
-      if Evd.in_dom (evar_map env) sp then
-        if defined_const env k then
-          whd_ise env (const_or_ex_value env k)
-        else
-          errorlabstrm "whd_ise"
-            [< 'sTR"There is an unknown subterm I cannot solve" >]
-      else 
-	k
-  | DOP2(Cast,c,_) -> whd_ise env c
-  | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
-  | c -> c
-
-
-(* 2- undefined existentials are left unchanged *)
-let rec whd_ise1 env = function
-  | (DOPN(Const sp,_) as k) ->
-      if Evd.in_dom (evar_map env) sp & defined_const env k then
-        whd_ise1 env (const_or_ex_value env k)
-      else 
-	k
-  | DOP2(Cast,c,_) -> whd_ise1 env c
-  | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
-  | c -> c
-
-let nf_ise1 env = strong (whd_ise1 env) env
-
-(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
- * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
-
-let rec whd_ise1_metas env = function
-  | (DOPN(Const sp,_) as k) ->
-      if Evd.in_dom (evar_map env) sp then
-	if defined_const env k then
-      	  whd_ise1_metas env (const_or_ex_value env k)
-	else 
-      	  let m = DOP0(Meta (new_meta())) in
-	  DOP2(Cast,m,const_or_ex_type env k)
-      else
-	k
-  | DOP2(Cast,c,_) -> whd_ise1_metas env c
-  | c -> c
 
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 8b2d988c3a..f24431a2f7 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -8,7 +8,6 @@ open Term
 open Univ
 open Environ
 open Closure
-open Evd
 (*i*)
 
 (* Reduction Functions. *)
@@ -17,10 +16,10 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = 'a unsafe_env -> constr -> constr
+type 'a reduction_function = unsafe_env -> constr -> constr
 
 type 'a stack_reduction_function = 
-    'a unsafe_env -> constr -> constr list -> constr * constr list
+    unsafe_env -> constr -> constr list -> constr * constr list
 
 val whd_stack : 'a stack_reduction_function
 
@@ -73,41 +72,31 @@ val whd_betadeltaiotaeta : 'a reduction_function
 val beta_applist : (constr * constr list) -> constr
 
 
-(*s Special-Purpose Reduction Functions *)
-val whd_meta : 'a reduction_function
-val plain_instance : 'a reduction_function
-val instance : 'a reduction_function
-
-val whd_ise : 'a reduction_function
-val whd_ise1 : 'a reduction_function
-val nf_ise1 : 'a reduction_function
-val whd_ise1_metas : 'a reduction_function
-
-val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr
+val hnf_prod_app : unsafe_env -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
-  'c unsafe_env -> string -> constr -> constr array -> constr
+  unsafe_env -> string -> constr -> constr array -> constr
 val hnf_prod_applist : 
-  'c unsafe_env -> string -> constr -> constr list -> constr
+  unsafe_env -> string -> constr -> constr list -> constr
 val hnf_lam_app : 
-  'c unsafe_env -> string -> constr -> constr -> constr
+  unsafe_env -> string -> constr -> constr -> constr
 val hnf_lam_appvect : 
-  'c unsafe_env -> string -> constr -> constr array -> constr
+  unsafe_env -> string -> constr -> constr array -> constr
 val hnf_lam_applist : 
-  'c unsafe_env -> string -> constr -> constr list -> constr
-val splay_prod : 'c unsafe_env -> constr -> (name * constr) list * constr
-val decomp_prod : 'c unsafe_env -> constr -> int * constr
+  unsafe_env -> string -> constr -> constr list -> constr
+val splay_prod : unsafe_env -> constr -> (name * constr) list * constr
+val decomp_prod : unsafe_env -> constr -> int * constr
 val decomp_n_prod : 
-  'c unsafe_env -> int -> constr -> ((name * constr) list) * constr
-
-val is_arity : 'c unsafe_env -> constr -> bool
-val is_info_arity : 'c unsafe_env -> constr -> bool
-val is_info_sort : 'c unsafe_env -> constr -> bool
-val is_logic_arity : 'c unsafe_env -> constr -> bool
-val is_type_arity : 'c unsafe_env -> constr -> bool
-val is_info_type : 'c unsafe_env -> typed_type -> bool
-val is_info_cast_type : 'c unsafe_env -> constr -> bool
-val contents_of_cast_type : 'c unsafe_env -> constr -> contents
-val poly_args : 'a unsafe_env -> constr -> int list
+  unsafe_env -> int -> constr -> ((name * constr) list) * constr
+
+val is_arity : unsafe_env -> constr -> bool
+val is_info_arity : unsafe_env -> constr -> bool
+val is_info_sort : unsafe_env -> constr -> bool
+val is_logic_arity : unsafe_env -> constr -> bool
+val is_type_arity : unsafe_env -> constr -> bool
+val is_info_type : unsafe_env -> typed_type -> bool
+val is_info_cast_type : unsafe_env -> constr -> bool
+val contents_of_cast_type : unsafe_env -> constr -> contents
+val poly_args : unsafe_env -> constr -> int list
 
 val whd_programs : 'a reduction_function
 
@@ -142,7 +131,7 @@ val convert_or : conversion_test -> conversion_test -> conversion_test
 val convert_forall2 : 
   ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
 
-type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints
+type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
 
 val fconv : conv_pb -> 'a conversion_function
 
@@ -153,27 +142,27 @@ val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 
 val conv_forall2 : 
-  'a conversion_function -> 'a unsafe_env 
+  'a conversion_function -> unsafe_env 
     -> constr array -> constr array -> constraints
 
 val conv_forall2_i : 
-  (int -> 'a conversion_function) -> 'a unsafe_env 
+  (int -> 'a conversion_function) -> unsafe_env 
     -> constr array -> constr array -> constraints
 
-val is_conv : 'a unsafe_env -> constr -> constr -> bool
-val is_conv_leq : 'a unsafe_env -> constr -> constr -> bool
+val is_conv : unsafe_env -> constr -> constr -> bool
+val is_conv_leq : unsafe_env -> constr -> constr -> bool
 
 (*s Obsolete Reduction Functions *)
 
-val hnf : 'a unsafe_env -> constr -> constr * constr list
+val hnf : unsafe_env -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
 val red_product : 'a reduction_function
-val find_mrectype : 'a unsafe_env -> constr -> constr * constr list
-val find_minductype : 'a unsafe_env -> constr -> constr * constr list
-val find_mcoinductype : 'a unsafe_env -> constr -> constr * constr list
-val check_mrectype_spec : 'a unsafe_env -> constr -> constr
-val minductype_spec : 'a unsafe_env -> constr -> constr
-val mrectype_spec : 'a unsafe_env -> constr -> constr
+val find_mrectype : unsafe_env -> constr -> constr * constr list
+val find_minductype : unsafe_env -> constr -> constr * constr list
+val find_mcoinductype : unsafe_env -> constr -> constr * constr list
+val check_mrectype_spec : unsafe_env -> constr -> constr
+val minductype_spec : unsafe_env -> constr -> constr
+val mrectype_spec : unsafe_env -> constr -> constr
 
 (* Special function, which keep the key casts under Fix and MutCase. *)
 val strip_all_casts : constr -> constr
diff --git a/kernel/term.ml b/kernel/term.ml
index 3871f6ce17..edc735ea7a 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -19,6 +19,7 @@ type 'a oper =
   | Cast | Prod | Lambda
   (* DOPN *)
   | AppL | Const of section_path | Abst of section_path
+  | Evar of section_path
   | MutInd of section_path * int
   | MutConstruct of (section_path * int) * int
   | MutCase of case_info
@@ -468,24 +469,23 @@ let destUntypedCoFix = function
 (******************)
 
 type kindOfTerm = 
-  | IsRel            of int
-  | IsMeta           of int
-  | IsVar            of identifier
-  | IsXtra           of string
-  | IsSort           of sorts
-  | IsCast           of constr*constr
-  | IsProd           of name*constr*constr
-  | IsLambda         of name*constr*constr
-  | IsAppL           of constr array
-  | IsConst          of section_path*constr array 
-  | IsAbst           of section_path*constr array
-  | IsMutInd         of section_path*int*constr array 
-  | IsMutConstruct   of section_path*int*int*constr array 
-  | IsMutCase        of case_info*constr*constr*(constr array)
-  | IsFix            of (int array)*int*
-                        (constr array)*(name list)*(constr array)
-  | IsCoFix          of int*(constr array) *
-                        (name list)*(constr array)
+  | IsRel          of int
+  | IsMeta         of int
+  | IsVar          of identifier
+  | IsXtra         of string
+  | IsSort         of sorts
+  | IsCast         of constr * constr
+  | IsProd         of name * constr * constr
+  | IsLambda       of name * constr * constr
+  | IsAppL         of constr array
+  | IsConst        of section_path * constr array 
+  | IsAbst         of section_path * constr array
+  | IsEvar         of section_path * constr array
+  | IsMutInd       of section_path * int * constr array 
+  | IsMutConstruct of section_path * int * int * constr array 
+  | IsMutCase      of case_info * constr * constr * constr array
+  | IsFix          of int array * int * constr array * name list * constr array
+  | IsCoFix        of int * constr array * name list * constr array
 
 
 (* Discriminates which kind of term is it.  
@@ -498,14 +498,15 @@ let kind_of_term c =
   match c with
     | Rel n                                -> IsRel n
     | VAR id                               -> IsVar id 
-    | DOP0 (Meta n)                        -> IsMeta  n
-    | DOP0 (Sort s)                        -> IsSort  s
+    | DOP0 (Meta n)                        -> IsMeta n
+    | DOP0 (Sort s)                        -> IsSort s
     | DOP0 (XTRA s)                        -> IsXtra s
-    | DOP2 (Cast, t1, t2)                  -> IsCast   (t1,t2)
+    | DOP2 (Cast, t1, t2)                  -> IsCast (t1,t2)
     | DOP2 (Prod, t1, (DLAM (x,t2)))       -> IsProd (x,t1,t2) 
     | DOP2 (Lambda, t1, (DLAM (x,t2)))     -> IsLambda (x,t1,t2)
     | DOPN (AppL,a)                        -> IsAppL a
-    | DOPN (Const  sp, a)                  -> IsConst (sp,a)
+    | DOPN (Const sp, a)                   -> IsConst (sp,a)
+    | DOPN (Evar sp, a)                   -> IsEvar (sp,a)
     | DOPN (Abst sp, a)                    -> IsAbst (sp, a)
     | DOPN (MutInd (sp,i), l)              -> IsMutInd (sp,i,l)
     | DOPN (MutConstruct ((sp,i), j),l)    -> IsMutConstruct (sp,i,j,l)
@@ -578,7 +579,7 @@ and appvectc f l = appvect (f,l)
 (* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
  * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
 let rec to_lambda n prod =
-  if n=0 then 
+  if n = 0 then 
     prod 
   else 
     match prod with 
@@ -601,8 +602,7 @@ let rec to_prod n lam =
  * [prod_app  s (Prod(_,B)) N --> B[N]
  * with an strip_outer_cast on the first argument to produce a product.
  * if this does not work, then we use the string S as part of our
- * error message.
- *)
+ * error message. *)
 
 let prod_app s t n =
   match strip_outer_cast t with
@@ -646,32 +646,28 @@ let decompose_lam =
 (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_prod_n n =
-  if n < 0 then 
-    error "decompose_prod_n: integer parameter must be positive"
-  else
-    let rec prodec_rec l n c = 
-      if n=0 then l,c 
-      else match c with 
-	| DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) (n-1) c
-        | DOP2(Cast,c,_)         -> prodec_rec l n c
-        | c -> error "decompose_prod_n: not enough products"
-    in 
-    prodec_rec [] n 
+  if n < 0 then error "decompose_prod_n: integer parameter must be positive";
+  let rec prodec_rec l n c = 
+    if n=0 then l,c 
+    else match c with 
+      | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) (n-1) c
+      | DOP2(Cast,c,_)         -> prodec_rec l n c
+      | c -> error "decompose_prod_n: not enough products"
+  in 
+  prodec_rec [] n 
 
 (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_lam_n n =
-  if n < 0 then
-    error "decompose_lam_n: integer parameter must be positive"
-  else 
-    let rec lamdec_rec l n c = 
-      if n=0 then l,c 
-      else match c with 
-        | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) (n-1) c
-        | DOP2(Cast,c,_)           -> lamdec_rec l n c
-        | c -> error "decompose_lam_n: not enough abstractions"
-    in 
-    lamdec_rec [] n 
+  if n < 0 then error "decompose_lam_n: integer parameter must be positive";
+  let rec lamdec_rec l n c = 
+    if n=0 then l,c 
+    else match c with 
+      | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) (n-1) c
+      | DOP2(Cast,c,_)           -> lamdec_rec l n c
+      | c -> error "decompose_lam_n: not enough abstractions"
+  in 
+  lamdec_rec [] n 
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
@@ -947,7 +943,7 @@ let whd_castapp x = applist(whd_castapp_stack x [])
 
 (* alpha conversion : ignore print names and casts *)
 let rec eq_constr_rec m n = 
-  if m = n then true else
+  (m = n) or
   match (strip_head_cast m,strip_head_cast n) with
     | (DOP2(Cast,c1,_),c2) 	       -> eq_constr_rec c1 c2
     | (c1,DOP2(Cast,c2,_))              -> eq_constr_rec c1 c2
diff --git a/kernel/term.mli b/kernel/term.mli
index c36df1f65b..8622b8f3f9 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -15,6 +15,7 @@ type 'a oper =
   | Sort of 'a
   | Cast | Prod | Lambda
   | AppL | Const of section_path | Abst of section_path
+  | Evar of section_path
   | MutInd of section_path * int
   | MutConstruct of (section_path * int) * int
   | MutCase of case_info
@@ -75,13 +76,13 @@ type kindOfTerm =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsAppL         of constr array
-  | IsConst        of section_path  * constr array
-  | IsAbst         of section_path  * constr array
+  | IsConst        of section_path * constr array
+  | IsAbst         of section_path * constr array
+  | IsEvar         of section_path * constr array
   | IsMutInd       of section_path * int * constr array
   | IsMutConstruct of section_path * int * int * constr array
   | IsMutCase      of case_info * constr * constr * constr array
-  | IsFix          of int array * int * constr array * name list *
-                      constr array
+  | IsFix          of int array * int * constr array * name list * constr array
   | IsCoFix        of int * constr array * name list * constr array
 
 (* Discriminates which kind of term is it.  
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 6632c172f2..7a1f232f17 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -31,43 +31,43 @@ type type_error =
 
 exception TypeError of path_kind * context * type_error
 
-val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b
+val error_unbound_rel : path_kind -> unsafe_env -> int -> 'b
 
-val error_cant_execute : path_kind -> 'a unsafe_env -> constr -> 'b
+val error_cant_execute : path_kind -> unsafe_env -> constr -> 'b
 
-val error_not_type : path_kind -> 'a unsafe_env -> constr -> 'b
+val error_not_type : path_kind -> unsafe_env -> constr -> 'b
 
-val error_assumption : path_kind -> 'a unsafe_env -> constr -> 'b
+val error_assumption : path_kind -> unsafe_env -> constr -> 'b
  
-val error_reference_variables : path_kind -> 'a unsafe_env -> identifier -> 'b
+val error_reference_variables : path_kind -> unsafe_env -> identifier -> 'b
 
 val error_elim_arity : 
-  path_kind -> 'a unsafe_env -> constr -> constr list -> constr 
+  path_kind -> unsafe_env -> constr -> constr list -> constr 
     -> constr -> constr -> (constr * constr * string) option -> 'b
 
 val error_case_not_inductive : 
-  path_kind -> 'a unsafe_env -> constr -> constr -> 'b
+  path_kind -> unsafe_env -> constr -> constr -> 'b
 
 val error_number_branches : 
-  path_kind -> 'a unsafe_env -> constr -> constr -> int -> 'b
+  path_kind -> unsafe_env -> constr -> constr -> int -> 'b
 
 val error_ill_formed_branch :
-  path_kind -> 'a unsafe_env -> constr -> int -> constr -> constr -> 'b
+  path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b
 
 val error_generalization :
-  path_kind -> 'a unsafe_env -> name * typed_type -> constr -> 'b
+  path_kind -> unsafe_env -> name * typed_type -> constr -> 'b
 
 val error_actual_type :
-  path_kind -> 'a unsafe_env -> constr -> constr -> constr -> 'b
+  path_kind -> unsafe_env -> constr -> constr -> constr -> 'b
 
 val error_cant_apply : 
-  path_kind -> 'a unsafe_env -> string -> unsafe_judgment 
+  path_kind -> unsafe_env -> string -> unsafe_judgment 
     -> unsafe_judgment list -> 'b
 
 val error_ill_formed_rec_body :
-  path_kind -> 'a unsafe_env -> std_ppcmds
+  path_kind -> unsafe_env -> std_ppcmds
     -> name list -> int -> constr array -> 'b
 
 val error_ill_typed_rec_body  :
-  path_kind -> 'a unsafe_env -> int -> name list -> unsafe_judgment array 
+  path_kind -> unsafe_env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> 'b
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f863a079f1..405b139bac 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -7,7 +7,6 @@ open Names
 open Univ
 open Generic
 open Term
-open Evd
 open Constant
 open Inductive
 open Sign
@@ -96,23 +95,6 @@ let type_of_constant env c =
   check_hyps (basename sp) env hyps;
   instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
 
-(* Existentials. *)
-
-let type_of_existential env c =
-  let (sp,args) = destConst c in
-  let info = Evd.map (evar_map env) sp in
-  let hyps = info.evar_hyps in
-  check_hyps (basename sp) env hyps;
-  instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args)
-
-(* Constants or existentials. *)
-
-let type_of_constant_or_existential env c =
-  if is_existential c then
-    type_of_existential env c
-  else
-    type_of_constant env c
-
 (* Inductive types. *)
 
 let instantiate_arity mis =
@@ -433,7 +415,7 @@ let apply_rel_list env nocheck argjl funj =
 (* Fixpoints. *)
 
 (* Checking function for terms containing existential variables.
- The function noccur_with_meta consideres the fact that
+ The function [noccur_with_meta] considers the fact that
  each existential variable (as well as each isevar)
  in the term appears applied to its local context,
  which may contain the CoFix variables. These occurrences of CoFix variables
@@ -441,13 +423,13 @@ let apply_rel_list env nocheck argjl funj =
 
 let noccur_with_meta sigma n m term = 
   let rec occur_rec n = function
-    | Rel(p) -> if n<=p & p<n+m then raise Occur
+    | Rel p -> if n<=p & p<n+m then raise Occur
     | VAR _ -> ()
     | DOPN(AppL,cl) ->
 	(match strip_outer_cast cl.(0) with
            | DOP0 (Meta _) -> ()
 	   | _ -> Array.iter (occur_rec n) cl)
-    | DOPN(Const sp, cl) when Evd.in_dom sigma sp -> ()
+    | DOPN(Const sp, cl) when Spset.mem sp sigma -> ()
     | DOPN(op,cl) -> Array.iter (occur_rec n) cl
     | DOPL(_,cl) -> List.iter (occur_rec n) cl
     | DOP0(_) -> ()
@@ -577,9 +559,9 @@ let is_subterm env lcx mind_recvec n lst c =
     false
 
 (* Auxiliary function: it checks a condition f depending on a deBrujin
- index  for a certain number of abstractions *)
+   index for a certain number of abstractions *)
 
-let rec check_subterm_rec_meta env vectn k def = 
+let rec check_subterm_rec_meta env sigma vectn k def = 
   (k < 0) or
   (let nfi = Array.length vectn in 
    (* check fi does not appear in the k+1 first abstractions, 
@@ -587,7 +569,7 @@ let rec check_subterm_rec_meta env vectn k def =
    let rec check_occur n def = 
      (match strip_outer_cast def with
 	| DOP2(Lambda,a,DLAM(_,b)) -> 
-	    if noccur_with_meta (evar_map env) n nfi a then
+	    if noccur_with_meta sigma n nfi a then
               if n = k+1 then (a,b) else check_occur (n+1) b
             else 
 	      error "Bad occurrence of recursive call"
@@ -605,7 +587,7 @@ let rec check_subterm_rec_meta env vectn k def =
    *)
    let rec check_rec_call n lst t = 
      (* n gives the index of the recursive variable *)
-     (noccur_with_meta (evar_map env) (n+k+1) nfi t) or 
+     (noccur_with_meta sigma (n+k+1) nfi t) or 
      (* no recursive call in the term *)
      (match whd_betadeltaiota_stack env t [] with 
 	| (Rel p,l) -> 
@@ -716,7 +698,7 @@ nvect is [|n1;..;nk|] which gives for each recursive definition
 the inductive-decreasing index 
 the function checks the convertibility of ti with Ai *)
 
-let check_fix env = function
+let check_fix env sigma = function
   | DOPN(Fix(nvect,j),vargs) -> 
       let nbfix = let nv = Array.length vargs in 
       if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
@@ -731,7 +713,9 @@ let check_fix env = function
 	let vlna = Array.of_list lna in
 	let check_type i = 
 	  try
-	    let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in ()
+	    let _ = 
+	      check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in 
+	    ()
 	  with UserError (s,str) ->
 	    error_ill_formed_rec_body CCI env str lna i vdefs 
 	in
@@ -744,7 +728,7 @@ let check_fix env = function
 let mind_nparams env i =
   let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
 
-let check_guard_rec_meta env nbfix def deftype = 
+let check_guard_rec_meta env sigma nbfix def deftype = 
   let rec codomain_is_coind c  =
     match whd_betadeltaiota env (strip_outer_cast c) with
       | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b 
@@ -758,9 +742,8 @@ let check_guard_rec_meta env nbfix def deftype =
   let (sp,tyi,_) = destMutInd mI in
   let lvlra = (mis_recargs (lookup_mind_specif mI env)) in
   let vlra = lvlra.(tyi) in  
-  let evd = evar_map env in
   let rec check_rec_call alreadygrd n vlra  t = 
-    if (noccur_with_meta evd n nbfix t) then
+    if noccur_with_meta sigma n nbfix t then
       true 
     else 
       match whd_betadeltaiota_stack env t [] with 
@@ -770,7 +753,7 @@ let check_guard_rec_meta env nbfix def deftype =
              if n <= p && p < n+nbfix then
 	       (* recursive call *)
                if alreadygrd then
-		 if List.for_all (noccur_with_meta evd n nbfix) l then
+		 if List.for_all (noccur_with_meta sigma n nbfix) l then
 		   true
 		 else 
 		   error "Nested recursive occurrences"
@@ -809,14 +792,14 @@ let check_guard_rec_meta env nbfix def deftype =
                                (process_args_of_constr lr lrar)
 				 
                        |  _::lrar  -> 
-                            if (noccur_with_meta evd n nbfix t) 
+                            if (noccur_with_meta sigma n nbfix t) 
                             then (process_args_of_constr lr lrar)
                             else error "Recursive call inside a non-recursive argument of constructor")
             in (process_args_of_constr realargs lra)
 		 
 		 
 	| (DOP2(Lambda,a,DLAM(_,b)),[]) -> 
-            if (noccur_with_meta evd n nbfix a) then
+            if (noccur_with_meta sigma n nbfix a) then
               check_rec_call alreadygrd (n+1)  vlra b
             else 
 	      error "Recursive call in the type of an abstraction"
@@ -834,7 +817,7 @@ let check_guard_rec_meta env nbfix def deftype =
             let (lna,vdefs) = decomp_DLAMV_name la ldef in
             let vlna = Array.of_list lna 
             in 
-	    if (array_for_all (noccur_with_meta evd n nbfix) varit) then
+	    if (array_for_all (noccur_with_meta sigma n nbfix) varit) then
               (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
               &&
               (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) 
@@ -843,9 +826,9 @@ let check_guard_rec_meta env nbfix def deftype =
 		
 	| (DOPN(MutCase _,_) as mc,l) -> 
             let (_,p,c,vrest) = destCase mc in
-            if (noccur_with_meta evd n nbfix p) then
-              if (noccur_with_meta evd n nbfix c) then
-		if (List.for_all (noccur_with_meta evd n nbfix) l) then
+            if (noccur_with_meta sigma n nbfix p) then
+              if (noccur_with_meta sigma n nbfix c) then
+		if (List.for_all (noccur_with_meta sigma n nbfix) l) then
 		  (array_for_all (check_rec_call alreadygrd n vlra) vrest)
 		else 
 		  error "Recursive call in the argument of a function defined by cases"        
@@ -862,7 +845,7 @@ let check_guard_rec_meta env nbfix def deftype =
 (* The  function which checks that the whole block of definitions 
    satisfies the guarded condition *)
 
-let check_cofix env f = 
+let check_cofix env sigma f = 
   match f with
     | DOPN(CoFix(j),vargs) -> 
 	let nbfix = let nv = Array.length vargs in 
@@ -877,14 +860,17 @@ let check_cofix env f =
 	let (lna,vdefs) = decomp_DLAMV_name la ldef in
 	let vlna = Array.of_list lna in
 	let check_type i = 
-	  (try 
-	     let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in ()
-	   with UserError (s,str) -> 
-	     error_ill_formed_rec_body CCI env str lna i vdefs) 
+	  try 
+	    let _ = 
+	      check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in 
+	    ()
+	  with UserError (s,str) -> 
+	    error_ill_formed_rec_body CCI env str lna i vdefs 
 	in
 	for i = 0 to nbfix-1 do check_type i done
     | _ -> assert false
 
+
 (* Checks the type of a (co)fixpoint.
    Fix and CoFix are typed the same way; only the guard condition differs. *)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 992a3a768d..a95b54b66e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -19,18 +19,18 @@ val j_val_only : unsafe_judgment -> constr
    constructs the typed type $t:s$, while [assumption_of_judgement env j]
    cosntructs the type type $c:t$, checking that $t$ is a sort. *)
 
-val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
-val assumption_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
+val typed_type_of_judgment : unsafe_env -> unsafe_judgment -> typed_type
+val assumption_of_judgment : unsafe_env -> unsafe_judgment -> typed_type
 
-val relative : 'a unsafe_env -> int -> unsafe_judgment
+val relative : unsafe_env -> int -> unsafe_judgment
 
-val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type
+val type_of_constant : unsafe_env -> constr -> typed_type
 
-val type_of_inductive : 'a unsafe_env -> constr -> typed_type
+val type_of_inductive : unsafe_env -> constr -> typed_type
 
-val type_of_constructor : 'a unsafe_env -> constr -> constr
+val type_of_constructor : unsafe_env -> constr -> constr
 
-val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment 
+val type_of_case : unsafe_env -> unsafe_judgment -> unsafe_judgment 
   -> unsafe_judgment array -> unsafe_judgment
 
 val type_of_prop_or_set : contents -> unsafe_judgment
@@ -38,22 +38,22 @@ val type_of_prop_or_set : contents -> unsafe_judgment
 val type_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
-  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+  unsafe_env -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val gen_rel :
-  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+  unsafe_env -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val cast_rel : 
-  'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+  unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
 
 val apply_rel_list : 
-  'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
+  unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
     -> unsafe_judgment * constraints
 
-val check_fix : 'a unsafe_env -> constr -> unit
-val check_cofix : 'a unsafe_env -> constr -> unit
+val check_fix : unsafe_env -> Spset.t -> constr -> unit
+val check_cofix : unsafe_env -> Spset.t -> constr -> unit
 
-val type_fixpoint : 'a unsafe_env -> name list -> typed_type array 
+val type_fixpoint : unsafe_env -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 46fbbf17c4..896d469c8c 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -40,18 +40,10 @@ type 'a mach_flags = {
 let rec execute mf env cstr =
   let cst0 = Constraint.empty in
   match kind_of_term cstr with
-    | IsMeta n ->
-       	let metaty =
-          try lookup_meta n env
-          with Not_found -> error "A variable remains non instanciated" 
-	in
-        (match kind_of_term metaty with
-           | IsCast (typ,kind) -> 
-	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0)
-           | _ ->
-	       let (jty,cst) = execute mf env metaty in
-	       let k = whd_betadeltaiotaeta env jty.uj_type in
-	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst))
+    | IsMeta _ ->
+	anomaly "the kernel does not understand metas"
+    | IsEvar _ ->
+	anomaly "the kernel does not understand existential variables"
 	
     | IsRel n -> 
 	(relative env n, cst0)
@@ -66,7 +58,7 @@ let rec execute mf env cstr =
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
     | IsConst _ ->
-        (make_judge cstr (type_of_constant_or_existential env cstr), cst0)
+        (make_judge cstr (type_of_constant env cstr), cst0)
 	  
     | IsMutInd _ ->
 	(make_judge cstr (type_of_inductive env cstr), cst0)
@@ -87,13 +79,13 @@ let rec execute mf env cstr =
           error "General Fixpoints not allowed";
         let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
-        check_fix env fix;
+        check_fix env Spset.empty fix;
 	(make_judge fix larv.(i), cst)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
         let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
-        check_cofix env cofix;
+        check_cofix env Spset.empty cofix;
 	(make_judge cofix larv.(i), cst)
 	  
     | IsSort (Prop c) -> 
@@ -239,13 +231,11 @@ let safe_machine_v env cv =
 
 (*s Safe environments. *)
 
-type 'a environment = 'a unsafe_env
+type environment = unsafe_env
 
 let empty_environment = empty_env
 
-let evar_map = evar_map
 let universes = universes
-let metamap = metamap
 let context = context
 
 let lookup_var = lookup_var
@@ -253,7 +243,6 @@ let lookup_rel = lookup_rel
 let lookup_constant = lookup_constant
 let lookup_mind = lookup_mind
 let lookup_mind_specif = lookup_mind_specif
-let lookup_meta = lookup_meta
 
 (* Insertion of variables (named and de Bruijn'ed). They are now typed before
    being added to the environment. *)
diff --git a/kernel/typing.mli b/kernel/typing.mli
index f93494a95b..10530d123b 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -6,7 +6,6 @@ open Pp
 open Names
 open Term
 open Univ
-open Evd
 open Sign
 open Constant
 open Inductive
@@ -19,36 +18,33 @@ open Typeops
   added. Internally, the datatype is still [unsafe_env]. We re-export the
   functions of [Environ] for the new type [environment]. *)
 
-type 'a environment
+type environment
 
-val empty_environment : 'a environment
+val empty_environment : environment
 
-val evar_map : 'a environment -> 'a evar_map
-val universes : 'a environment -> universes
-val metamap : 'a environment -> (int * constr) list
-val context : 'a environment -> context
+val universes : environment -> universes
+val context : environment -> context
 
-val push_var : identifier * constr -> 'a environment -> 'a environment
-val push_rel : name * constr -> 'a environment -> 'a environment
+val push_var : identifier * constr -> environment -> environment
+val push_rel : name * constr -> environment -> environment
 val add_constant : 
-  section_path -> constant_entry -> 'a environment -> 'a environment
+  section_path -> constant_entry -> environment -> environment
 val add_parameter :
-  section_path -> constr -> 'a environment -> 'a environment
+  section_path -> constr -> environment -> environment
 val add_mind : 
-  section_path -> mutual_inductive_entry -> 'a environment -> 'a environment
-val add_constraints : constraints -> 'a environment -> 'a environment
+  section_path -> mutual_inductive_entry -> environment -> environment
+val add_constraints : constraints -> environment -> environment
 
-val lookup_var : identifier -> 'a environment -> name * typed_type
-val lookup_rel : int -> 'a environment -> name * typed_type
-val lookup_constant : section_path -> 'a environment -> constant_body
-val lookup_mind : section_path -> 'a environment -> mutual_inductive_body
-val lookup_mind_specif : constr -> 'a environment -> mind_specif
-val lookup_meta : int -> 'a environment -> constr
+val lookup_var : identifier -> environment -> name * typed_type
+val lookup_rel : int -> environment -> name * typed_type
+val lookup_constant : section_path -> environment -> constant_body
+val lookup_mind : section_path -> environment -> mutual_inductive_body
+val lookup_mind_specif : constr -> environment -> mind_specif
 
-val export : 'a environment -> string -> compiled_env
-val import : compiled_env -> 'a environment -> 'a environment
+val export : environment -> string -> compiled_env
+val import : compiled_env -> environment -> environment
 
-val unsafe_env_of_env : 'a environment -> 'a unsafe_env
+val unsafe_env_of_env : environment -> unsafe_env
 
 (*s Typing without information. *)
 
@@ -58,20 +54,20 @@ val j_val : judgment -> constr
 val j_type : judgment -> constr
 val j_kind : judgment -> constr
 
-val safe_machine : 'a environment -> constr -> judgment * constraints
-val safe_machine_type : 'a environment -> constr -> typed_type
+val safe_machine : environment -> constr -> judgment * constraints
+val safe_machine_type : environment -> constr -> typed_type
 
-val fix_machine : 'a environment -> constr -> judgment * constraints
-val fix_machine_type : 'a environment -> constr -> typed_type
+val fix_machine : environment -> constr -> judgment * constraints
+val fix_machine_type : environment -> constr -> typed_type
 
-val unsafe_machine : 'a environment -> constr -> judgment * constraints
-val unsafe_machine_type : 'a environment -> constr -> typed_type
+val unsafe_machine : environment -> constr -> judgment * constraints
+val unsafe_machine_type : environment -> constr -> typed_type
 
-val type_of : 'a environment -> constr -> constr
+val type_of : environment -> constr -> constr
 
-val type_of_type : 'a environment -> constr -> constr
+val type_of_type : environment -> constr -> constr
 
-val unsafe_type_of : 'a environment -> constr -> constr
+val unsafe_type_of : environment -> constr -> constr
 
 
 (*s Typing with information (extraction). *)