environnement sur

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

21 files changed, 211 insertions, 458 deletions

diff --git a/.depend b/.depend
index 1f8d5b95c4..e4a9a95c5c 100644
--- a/.depend
+++ b/.depend
@@ -1,7 +1,3 @@
-attente/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/sign.cmi kernel/term.cmi 
-attente/printer.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/sign.cmi kernel/term.cmi 
 kernel/abstraction.cmi: kernel/names.cmi kernel/term.cmi 
 kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/names.cmi lib/pp.cmi kernel/term.cmi 
@@ -12,10 +8,6 @@ kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi
 kernel/generic.cmi: kernel/names.cmi lib/util.cmi 
 kernel/inductive.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 kernel/instantiate.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi 
-kernel/mach.cmi: kernel/environ.cmi kernel/machops.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/machops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \
-    kernel/univ.cmi 
 kernel/names.cmi: lib/pp.cmi 
 kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
@@ -25,16 +17,15 @@ kernel/term.cmi: lib/coqast.cmi kernel/generic.cmi kernel/names.cmi \
     kernel/univ.cmi 
 kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi 
+kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \
+    kernel/univ.cmi 
+kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi 
 lib/coqast.cmi: lib/dyn.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
 lib/util.cmi: lib/pp.cmi 
-attente/himsg.cmo: kernel/environ.cmi kernel/generic.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
-    attente/himsg.cmi 
-attente/himsg.cmx: kernel/environ.cmx kernel/generic.cmx lib/pp.cmx \
-    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
-    attente/himsg.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
@@ -75,24 +66,6 @@ kernel/instantiate.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
 kernel/instantiate.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/generic.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
     kernel/term.cmx lib/util.cmx kernel/instantiate.cmi 
-kernel/mach.cmo: kernel/environ.cmi kernel/generic.cmi kernel/machops.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
-    kernel/mach.cmi 
-kernel/mach.cmx: kernel/environ.cmx kernel/generic.cmx kernel/machops.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
-    kernel/mach.cmi 
-kernel/machops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
-    kernel/machops.cmi 
-kernel/machops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
-    kernel/machops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi 
 kernel/reduction.cmo: kernel/closure.cmi kernel/constant.cmi \
@@ -119,6 +92,24 @@ kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
 kernel/type_errors.cmx: kernel/environ.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmi 
+kernel/typeops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/typeops.cmi 
+kernel/typeops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
+    kernel/typeops.cmi 
+kernel/typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/generic.cmi \
+    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+    kernel/univ.cmi lib/util.cmi kernel/typing.cmi 
+kernel/typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/generic.cmx \
+    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+    kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+    kernel/univ.cmx lib/util.cmx kernel/typing.cmi 
 kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi 
 kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi 
 lib/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi lib/coqast.cmi 
diff --git a/Makefile b/Makefile
index d33ff7060d..894e7b9ef0 100644
--- a/Makefile
+++ b/Makefile
@@ -30,7 +30,7 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \
        kernel/environ.cmo kernel/instantiate.cmo \
        kernel/closure.cmo kernel/reduction.cmo \
-       kernel/type_errors.cmo kernel/machops.cmo kernel/mach.cmo
+       kernel/type_errors.cmo kernel/typeops.cmo kernel/typing.cmo
 
 OBJS=$(CONFIG) $(LIB) $(KERNEL)
 
diff --git a/dev/changements.txt b/dev/changements.txt
index 424132329b..039fcf210f 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -16,6 +16,10 @@ Changements dans les types de données :
   dans Generic: free_rels : constr -> int Listset.t
                   devient : constr -> Intset.t
 
+  type_judgement ->  typed_type
+  environment    ->  context
+  context        ->  typed_type signature
+
 Changements dans les fonctions :
 --------------------------------
 
diff --git a/doc/intro.tex b/doc/intro.tex
index a598ba6e77..c2e59566bc 100644
--- a/doc/intro.tex
+++ b/doc/intro.tex
@@ -1,2 +1,8 @@
 
-\ocwsection This is \Coq, a proof assistant for the \CCI.
\ No newline at end of file
+\ocwsection This is \Coq, a proof assistant for the \CCI.
+
+% \input{epsf}
+% \epsfxsize=5cm
+% \epsfysize=10cm
+% \hspace*{2cm}\vspace*{4cm}%
+% \epsfbox{kernel.graph.ps}
diff --git a/kernel/constant.ml b/kernel/constant.ml
index 0b52af6956..766fbb7354 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -16,17 +16,19 @@ type recipe =
   | Cooked of constr
   | Recipe of discharge_recipe
 
+type constant_entry = {
+  const_entry_body : constr;
+  const_entry_type : constr }
+
 type constant_body = {
   const_kind : path_kind;
   const_body : recipe ref option;
   const_type : typed_type;
-  const_hyps : context;
+  const_hyps : typed_type signature;
   mutable const_opaque : bool;
   mutable const_eval : ((int * constr) list * int * bool) option option;
 }
 
-type constant_entry = section_path * constant_body
-
 let is_defined cb = 
   match cb.const_body with Some _ -> true | _ -> false
 
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 60607cef25..d33dc5a859 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -11,17 +11,19 @@ type recipe =
   | Cooked of constr
   | Recipe of discharge_recipe
 
+type constant_entry = {
+  const_entry_body : constr;
+  const_entry_type : constr }
+
 type constant_body = {
   const_kind : path_kind;
   const_body : recipe ref option;
   const_type : typed_type;
-  const_hyps : context;
+  const_hyps : typed_type signature;
   mutable const_opaque : bool;
   mutable const_eval : ((int * constr) list * int * bool) option option;
 }
 
-type constant_entry = section_path * constant_body
-
 val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e84d8f296d..2b00e90d20 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -20,7 +20,7 @@ type globals = {
   env_abstractions : abstraction_body Spmap.t }
 
 type 'a unsafe_env = {
-  env_context : environment;
+  env_context : context;
   env_globals : globals;
   env_sigma : 'a evar_map;
   env_metamap : (int * constr) list;
@@ -42,12 +42,12 @@ let push_rel idrel env =
 let set_universes g env =
   if env.env_universes == g then env else { env with env_universes = g }
 
-let add_constant (sp,cb) env =
+let add_constant sp cb env =
   let new_constants = Spmap.add sp cb env.env_globals.env_constants in
   let new_globals = { env.env_globals with env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-let add_mind (sp,mib) env =
+let add_mind sp mib env =
   let new_inds = Spmap.add sp mib env.env_globals.env_inductives in
   let new_globals = { env.env_globals with env_inductives = new_inds } in
   { env with env_globals = new_globals }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 686e871795..4c1e23d035 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -14,13 +14,15 @@ type 'a 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 -> environment
+val context : 'a 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_constant : constant_entry -> 'a unsafe_env -> 'a unsafe_env
-val add_mind : mutual_inductive_entry -> 'a unsafe_env -> 'a unsafe_env
+val add_constant : 
+  section_path -> constant_body -> 'a unsafe_env -> 'a unsafe_env
+val add_mind : 
+  section_path -> mutual_inductive_body -> 'a unsafe_env -> 'a unsafe_env
 
 val new_meta : unit -> int
 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 24a50afa80..e5197db4e2 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -13,10 +13,10 @@ type evar_body =
   | EVAR_DEFINED of constr
 
 type 'a evar_info = {
-  evar_concl : typed_type;        (* the type of the evar ...          *)
-  evar_hyps  : context;           (* ... under a certain signature     *)
-  evar_body  : evar_body;         (* its definition                    *) 
-  evar_info  : 'a option }        (* any other necessary information   *)
+  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
 
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 899abb2034..696fcdd3b3 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -20,7 +20,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : typed_type;
-  evar_hyps  : context;
+  evar_hyps  : typed_type signature;
   evar_body  : evar_body;
   evar_info  : 'a option }
 
@@ -36,7 +36,8 @@ 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 -> context -> typed_type -> 'a evar_map
+  'a evar_map -> section_path -> typed_type signature -> typed_type 
+    -> 'a evar_map
 
 val define : 'a evar_map -> section_path -> constr -> 'a evar_map
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2aedc8dfd0..cb4b3f6556 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -31,7 +31,9 @@ type mutual_inductive_body = {
   mind_singl : constr option;
   mind_nparams : int }
 
-type mutual_inductive_entry = section_path * mutual_inductive_body
+type mutual_inductive_entry = {
+  mind_entry_params : (identifier * constr) list;
+  mind_entry_inds : (identifier * constr * (identifier * constr) list) list }
 
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 7f2887f200..e57c4d295e 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -31,7 +31,9 @@ type mutual_inductive_body = {
   mind_singl : constr option;
   mind_nparams : int }
 
-type mutual_inductive_entry = section_path * mutual_inductive_body
+type mutual_inductive_entry = {
+  mind_entry_params : (identifier * constr) list;
+  mind_entry_inds : (identifier * constr * (identifier * constr) list) list }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index c0e8658120..9c2ffedb2f 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -233,6 +233,5 @@ let lookup_id id env =
 
 
 type 'b assumptions = (typed_type,'b) env
-type environment = (typed_type,typed_type) env
-type context = typed_type signature
+type context = (typed_type,typed_type) env
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index ebf98a8f41..c9e1fb565f 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -78,6 +78,5 @@ val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
 
 
 type 'b assumptions = (typed_type,'b) env
-type environment = (typed_type,typed_type) env
-type context = typed_type signature
+type context = (typed_type,typed_type) env
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 6949940a48..f99a026104 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -21,13 +21,13 @@ type type_error =
   | NumberBranches of constr * constr * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * typed_type) * constr
-  | ActualType of unsafe_judgment * unsafe_judgment
+  | ActualType of constr * constr * constr
   | CantAply of string * unsafe_judgment * unsafe_judgment list
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
 
-exception TypeError of path_kind * environment * type_error
+exception TypeError of path_kind * context * type_error
 
 let error_unbound_rel k env n =
   raise (TypeError (k, context env, UnboundRel n))
@@ -59,8 +59,8 @@ let error_ill_formed_branch k env c i actty expty =
 let error_generalization k env nvar c =
   raise (TypeError (k, context env, Generalization (nvar,c)))
 
-let error_actual_type k env cj tj =
-  raise (TypeError (k, context env, ActualType (cj,tj)))
+let error_actual_type k env c actty expty =
+  raise (TypeError (k, context env, ActualType (c,actty,expty)))
 
 let error_cant_apply k env s rator randl =
   raise (TypeError (k, context env, CantAply (s,rator,randl)))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index cec8b78184..76bf18cc32 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -21,13 +21,13 @@ type type_error =
   | NumberBranches of constr * constr * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * typed_type) * constr
-  | ActualType of unsafe_judgment * unsafe_judgment
+  | ActualType of constr * constr * constr
   | CantAply of string * unsafe_judgment * unsafe_judgment list
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
 
-exception TypeError of path_kind * environment * type_error
+exception TypeError of path_kind * context * type_error
 
 val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b
 
@@ -56,7 +56,7 @@ val error_generalization :
   path_kind -> 'a unsafe_env -> name * typed_type -> constr -> 'b
 
 val error_actual_type :
-  path_kind -> 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> 'b
+  path_kind -> 'a unsafe_env -> constr -> constr -> constr -> 'b
 
 val error_cant_apply : 
   path_kind -> 'a unsafe_env -> string -> unsafe_judgment 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 23bac0b277..178963c48e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -404,7 +404,7 @@ let cast_rel env cj tj =
       uj_type = tj.uj_val;
       uj_kind = whd_betadeltaiota env tj.uj_type }
   else 
-    error_actual_type CCI env cj tj
+    error_actual_type CCI env cj.uj_val cj.uj_type tj.uj_val
 
 (* Type of an application. *)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 1a3b729c29..5ddb8031ed 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -16,6 +16,7 @@ val make_judge : constr -> typed_type -> unsafe_judgment
 val j_val_only : unsafe_judgment -> constr
 
 val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
+val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type
 
 val relative : 'a unsafe_env -> int -> unsafe_judgment
 
@@ -32,8 +33,6 @@ val type_of_prop_or_set : contents -> unsafe_judgment
 
 val type_of_type : universe -> universes -> unsafe_judgment * universes
 
-val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type
-
 val abs_rel : 
   'a unsafe_env -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * universes
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 2311fb9992..ebae3faf93 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -9,9 +9,11 @@ open Generic
 open Term
 open Reduction
 open Sign
+open Constant
+open Inductive
 open Environ
 open Type_errors
-open Machops
+open Typeops
 
 (* Fonctions temporaires pour relier la forme castée de la forme jugement *)
 
@@ -230,371 +232,95 @@ let unsafe_type_of_type env c =
   let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
 
 
+(*s Safe environments. *)
+
+type 'a environment = 'a unsafe_env
+
+let evar_map = evar_map
+let universes = universes
+let metamap = metamap
+let context = context
+
+let lookup_var = lookup_var
+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
+
+let push_rel_or_var push (id,ty) env =
+  let (j,u) = safe_machine env ty.body in
+  let env' = set_universes u env in
+  let expty = DOP0(Sort ty.typ) in
+  match conv env' j.uj_type expty with
+    | Convertible u' -> push (id,ty) (set_universes u' env')
+    | NotConvertible -> error_actual_type CCI env ty.body j.uj_type expty
+
+let push_var nvar env = push_rel_or_var push_var nvar env
+
+let push_rel nrel env = push_rel_or_var push_rel nrel env
+
+let add_constant sp ce env =
+  let (jb,u) = safe_machine env ce.const_entry_body in
+  let env' = set_universes u env in
+  let (jt,u') = safe_machine env ce.const_entry_type in
+  let env'' = set_universes u' env' in
+  match conv env'' jb.uj_type jt.uj_val with
+    | Convertible u'' -> 
+	let cb = { 
+	  const_kind = kind_of_path sp;
+	  const_body = Some (ref (Cooked ce.const_entry_body));
+	  const_type = typed_type_of_judgment env'' jt;
+	  const_hyps = get_globals (context env);
+	  const_opaque = false;
+	  const_eval = None } 
+	in
+	add_constant sp cb (set_universes u'' env'')
+    | NotConvertible -> 
+	error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+
+let type_from_judgment env j =
+  match whd_betadeltaiota env j.uj_kind with
+    | DOP0(Sort s) -> { body = j.uj_type; typ = s }
+    | _ -> error_not_type CCI env j.uj_type (* shouldn't happen *)
+
+let add_parameter sp c env =
+  let (j,u) = safe_machine env c in
+  let env' = set_universes u env in
+  let cb = {
+    const_kind = kind_of_path sp;
+    const_body = Some (ref (Cooked c));
+    const_type = type_from_judgment env' j;
+    const_hyps = get_globals (context env);
+    const_opaque = false;
+    const_eval = None } 
+  in
+  Environ.add_constant sp cb env'
+
+let add_mind sp me env =
+  let name_params = 
+    List.map (fun (id,c) -> (Name id, c)) me.mind_entry_params in
+  (* just to check the params *)
+  let env_params =
+    List.fold_left 
+      (fun env (id,c) ->
+	 let (j,u) = safe_machine env c in
+	 let env' = set_universes u env in
+	 Environ.push_var (id, assumption_of_judgement env' j) env')
+      env me.mind_entry_params
+  in
+  let env_arities =
+    List.fold_left 
+      (fun env (id,ar,_) -> 
+	 let (j,u) = safe_machine env (prod_it ar name_params) in
+	 let env' = set_universes u env in
+	 Environ.push_var (id, assumption_of_judgement env' j) env')
+      env me.mind_entry_inds
+  in
+  env_arities
+
+type judgment = unsafe_judgment
+
 (*s Machines with information. *)
 
 type information = Logic | Inf of unsafe_judgment
-
-(*i
-let implicit_judgment = {body=mkImplicit;typ=implicit_sort}
-
-let add_inf_rel (na,inf) env =
-  match inf with
-      Logic -> add_rel (na,implicit_judgment) env
-    | Inf j -> add_rel (na,tjudge_of_judge j) env
-
-
-let fw_mutind sigma fenv k =
-  let (sp,x,args) = destMutInd k in
-  let mis = mind_specif_of_mind k in
-    match mis_singl mis with 
-	Some a -> Some (a,true)
-      | None ->
-	  if is_info_cast_type sigma (mis_arity mis) then
-	    let infK =
-              global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x)))
-	    in Some (infK,false)
-	  else None
-
-let inf_of_mind sigma fenv mind = 
-  try
-    match fw_mutind sigma fenv mind with
-        Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK)
-      | None -> Logic
-  with
-      Not_found | Failure _ -> 
-	anomaly "cannot convert an inductive to an finductive"
-
-let inf_mconstructor (sigma,metamap) fenv k = 
-  let (sp,x,i,cl) = destMutConstruct k in
-  let mind = mkMutInd sp x cl in 
-    (match fw_mutind sigma fenv mind with
-         None -> Logic
-       | Some(infi,singl) ->
-	   (match mind_lamexp mind with
-	      | Some clamexp ->
-		  if singl
-		  then Inf(cast_fmachine (sigma,[]) fenv clamexp)
-		  else
-		    let (infsp, infx, infcl) = destMutInd infi in
-		    let infmconstructor = mkMutConstruct infsp infx i infcl in
-		    let infval = subst1 infmconstructor clamexp in
-		      Inf (cast_fmachine (sigma,fst metamap) fenv infval)
-	      | _ -> assert false))
-
-
-exception DefinedExtraction
-
-(* when c is an evaluable constant with an extraction which 
-   contains an implicit, gives the value of the c constant
-   otherwise raise DefinedExtraction
-*)
-
-let value_implicit_const sigma c cinf = 
-  match c with DOPN(Const(_),_) -> 
-    if evaluable_const sigma c then 
-      let cv = const_value sigma cinf in 
-	if is_implicit cv (* or contains_implicit sigma cv *)
-	then const_value sigma c 
-	else raise DefinedExtraction
-    else raise DefinedExtraction
-    | _ -> raise DefinedExtraction
-
-let unsafe_infmachine (sigma,metamap) env fenv c = 
-  let rec infexec env fenv cstr = match cstr with
-       DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic
-    |  DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic
-    |  DOP2(Cast,c,_) -> infexec env fenv c
-    |  DOP0(Meta n) ->
-         (match List.assoc n (snd metamap) with
-             Logic -> Logic
-           | Inf j -> Inf{uj_val=DOP0(Meta n);
-                          uj_type=j.uj_val;
-                          uj_kind = hnf_constr sigma j.uj_type})
-
-    | Rel n ->
-        inf_rel fenv
-          (contents_of_type sigma (snd (lookup_rel n env))) n
-
-    | VAR str ->
-        inf_var fenv
-          (contents_of_type sigma (snd(lookup_glob str env))) str
-
-    | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr
-
-    | DOPN(Abst _,_) ->
-        if evaluable_abst cstr then infexec env fenv (abst_value cstr)
-        else error "cannot extract from an unevaluable abstraction"
-
-    | DOP0(Sort s) -> inf_sort s
-
-    | DOPN(AppL,tl) ->
-        let c1 =  (hd_vect tl)
-        and cl = tl_vect tl in
-          let funinf = infexec env fenv c1 in
-            (match funinf with Logic -> Logic
-	      | Inf(j) -> let cinf = j.uj_val in
-             (* try to expand constants corresponding 
-		    to non extractable terms *)
-	      (try if is_extraction_expanded() then 
-		 let valcte = value_implicit_const sigma c1 cinf 
-		 in infexec env fenv (whd_betaiota (appvect(valcte,cl))) 
-	       else raise DefinedExtraction
-               with DefinedExtraction -> 
-		 let argsinf = Array.map (infexec env fenv) cl
-		 in it_vect inf_apply funinf argsinf))
-
-    | DOP2(Lambda,c1,DLAM(name,c2)) ->
-        let varinf = infexec env fenv c1 in
-        let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
-                        (add_inf_rel (name,varinf) fenv) c2
-        in inf_abs_rel name bodyinf varinf
-
-    | DOP2(Prod,c1,DLAM(name,c2)) ->
-        let c1inf = infexec env fenv c1 in
-        let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
-                      (add_inf_rel (name,c1inf) fenv) c2
-        in inf_gen_rel name c2inf c1inf
-
-    | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr
-
-    | DOPN(MutConstruct _,_) ->
-        inf_mconstructor (sigma,metamap) fenv cstr
-
-    | DOPN(Fix(vn,i),cl) ->
-        let lar = Array.sub cl 0 ((Array.length cl) - 1) in
-        let inflar = Array.map (infexec env fenv) lar in
-        let infAi = inflar.(i) in 
-          (match infAi with 
-              Logic   -> Logic 
-            | Inf aij ->
-                let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in
-                let (new_env,new_fenv) =
-                  it_vect2
-                    (fun (ne,nfe) fk ak -> 
-                       (add_rel (fk,tjudge_of_cast sigma ak) ne,
-                        let infAk = infexec ne nfe ak
-                        in (add_inf_rel (fk,infAk) nfe)))
-                    (env,fenv)
-                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
-(* a special function to localize the recursive index in the extracted term *)
-                let rec exec_def ne nfe n def = 
-                  (match hnf_constr sigma def with 
-                      DOP2(Lambda,c1,DLAM(name,c2)) ->
-                        let varinf = infexec ne nfe c1 in
-                        let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) 
-                        and nfe' = add_inf_rel (name,varinf) nfe in
-                          if n = 0 then
-                            let infc2 = infexec ne' nfe' c2 
-                            in let infdef = inf_abs_rel name infc2 varinf
-                               and index =
-                                 if varinf = Logic then -1
-                        (* the recursive call was on a non-informative term *) 
-                                 else 0 in (infdef,index)
-                          else
-                            let bodyinf,countl = 
-                              exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) 
-                                (add_inf_rel (name,varinf) nfe) (n-1) c2 in
-                            let (infabs,abs) =
-                              inf_abs_rel_count name bodyinf varinf
-                            in (infabs,
-                                if abs = ERASE then countl
-                                else if countl<0 then countl-1
-                                else countl+1)
-                    | _ -> anomaly "exec_def : should be a lambda") in
-                let infdefs_ind =
-                  map2_vect (exec_def new_env new_fenv) vn ldefs
-                in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind)
-
-    | DOPN(CoFix i,cl) ->
-        let lar    = Array.sub cl 0 ((Array.length cl) - 1) in 
-        let inflar = Array.map (infexec env fenv) lar in
-        let infAi  = inflar.(i) in
-          (match infAi with 
-              Logic   -> Logic 
-            | Inf aij -> 
-                let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in 
-                let (new_env,new_fenv) = 
-                  it_vect2 (fun (ne,nfe) fk ak -> 
-                              (add_rel (fk,tjudge_of_cast sigma ak) ne, 
-                               let infAk = infexec ne nfe ak
-                               in (add_inf_rel (fk,infAk) nfe)))
-                    (env,fenv) 
-                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
-                                   
-                let infdefs = Array.map (infexec new_env new_fenv) ldefs 
-                in  inf_cofix sigma i aij.uj_type lfi inflar infdefs)
-
-    | DOPN(MutCase _,_) ->
-        let (ci,p,c,lf) = destCase cstr in
-        let pinf = infexec env fenv p in 
-          (match pinf with
-              Logic  -> Logic 
-            | Inf pj -> 
-		if is_extraction_expanded() then 
-		  let (d,l) = whd_betadeltaiota_stack sigma c [] in 
-                 (match d with (DOPN(MutConstruct(_,_),_)) ->
-		    let cstr' = 
-		      DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf)
-		    in infexec env fenv (whd_betaiota cstr')
-		    | _ -> 
-                  let cinf = infexec env fenv c
-                  and lfinf = Array.map (infexec env fenv) lf
-                  in inf_mutcase fenv sigma pj ci cinf lfinf
-		 )
-               else let cinf = infexec env fenv c
-                  and lfinf = Array.map (infexec env fenv) lf
-                  in inf_mutcase fenv sigma pj ci cinf lfinf)
-	 
-    | _ -> error "Cannot extract information"
-  in infexec env fenv c
-
-
-let core_infmachine meta env fenv c =
-  try unsafe_infmachine meta env fenv c
-  with (UserError _ | Failure _) -> Logic
-
-(* WITH INFORMATION *)
-(* does not check anymore that extracted terms are well-formed *)
-let judgement_infmachine meta env fenv c ct = 
-  try
-    match unsafe_infmachine meta env fenv c with
-        Inf infj ->
-          let inftyp =
-            try unsafe_infmachine meta env fenv ct
-            with (UserError _ | Failure _) ->
-              (warning "Failed to extract in type"; Logic)
-          in (match inftyp with
-                  Inf infjt ->
-                    Inf{uj_val=infj.uj_val;
-                        uj_type=infjt.uj_val;
-                        uj_kind=infj.uj_kind}
-                | Logic -> Inf infj)
-      | Logic -> Logic
-  with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic)
-
-let infmachine_type nocheck (sigma,metamap) env fenv constr =
-  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
-  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
-  let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in
-  let inf = 
-    if is_info_type sigma t then (* Case the term is informative *)
-      let uniarc = get_uniarc () in
-      let infjt =
-        judgement_infmachine
-          (sigma,(constr_metamap,inf_metamap)) env fenv 
-	  t.body 
-	  (DOP0 (Sort t.typ)) in
-      let _ = set_uniarc uniarc in
-        infjt
-    else Logic
-
-  in hash_jpair_type
-       ({body = strip_all_casts t.body; typ = t.typ},
-        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
-                            uj_type = nf_beta j.uj_type;
-                            uj_kind = j.uj_kind }) inf))
-
-let infmachine nocheck (sigma,metamap) env fenv constr =
-  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
-  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
-  let j = core_fmachine nocheck (sigma,constr_metamap) env constr in
-  let inf = 
-    if is_info_judge sigma j then (* Case the term is informative *)
-      let uniarc = get_uniarc () in
-      let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in
-      let infjt =
-        judgement_infmachine
-          (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in
-      let _ = set_uniarc uniarc in
-        infjt
-    else Logic
-
-  in hash_jpair
-       ({uj_val = strip_all_casts j.uj_val;
-         uj_type = strip_all_casts j.uj_type;
-         uj_kind = j.uj_kind},
-        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
-                            uj_type = nf_beta j.uj_type;
-                            uj_kind = j.uj_kind }) inf))
-
-
-let jsign_of_sign sigma sign =
-  sign_it
-    (fun id a (sign,fsign) ->
-      let sign' = add_sign (id,a) sign in
-      let fsign' =
-        match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body
- 	with
-          (_,Logic) -> fsign
-        | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign
-      in (sign',fsign'))
-    sign (([],[]),([],[]))
-
-
-let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign)
-
-let infexemeta_type sigma metamap (env,fenv) c =
-  infmachine_type true (sigma,metamap) env fenv c
-
-let infexecute_rec_type sigma (env,fenv) c =
-  infmachine_type false (sigma,[]) env fenv c
-
-let infexecute_type sigma (sign,fsign) c =
-  infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c
-
-let infexemeta sigma metamap (env,fenv) c =
-  infmachine true (sigma,metamap) env fenv c
-
-let infexecute_rec sigma (env,fenv) c =
-  infmachine false (sigma,[]) env fenv c
-
-let infexecute sigma (sign,fsign) c =
-  infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c
-
-(* A adapter pour les nouveaux env
-let fvar_type sigma (sign,fsign) v = 
-  let na = destVar v in
-  let varty = (snd(lookup_sign na sign))
-  in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with
-      Inf ft -> ft.uj_val
-    | Logic -> invalid_arg "Fvar with a non-informative type (1)!"
-
-*)
-
-(* MACHINE WITH UNIVERSES *)
-(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab,
-   recuperer le graphe local, et restaurer l'acien graphe global *)
-
-let whd_instuni = function
-    DOP0(Sort(Type(u))) ->
-      let u = (if u = dummy_univ then new_univ() else u)
-      in DOP0(Sort(Type(u)))
-  | c -> c
-
-(* Instantiate universes: replace all dummy_univ by fresh universes.
-   This is already done by the machine.
-   Indtypes instantiates the universes itself, because in the case of
-   large constructor, additionnal constraints must be considered. *)
-let instantiate_universes c = strong whd_instuni c
-
-
-(* sp est le nom de la constante pour laquelle il faut que c soit bien type.
-   Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles
-   independamment.
-   Au lieu de sp, Lib.cwd() serait peut-etre suffisant.
-   Cela eviterai de donner un section-path quand on veut typer. *)
-let fexecute_type_with_univ sigma sign sp c =
-  with_universes (fexecute_type sigma sign) (sp,initial_universes,c) 
-
-
-let fexecute_with_univ sigma sign sp c =
-  with_universes (fexecute sigma sign) (sp,initial_universes,c) 
-
-
-let infexecute_type_with_univ sigma psign sp c =
-  with_universes (infexecute_type sigma psign) (sp,initial_universes,c) 
-
-
-let infexecute_with_univ sigma psign sp c =
-  with_universes (infexecute sigma psign) (sp,initial_universes,c) 
-i*)
diff --git a/kernel/typing.mli b/kernel/typing.mli
index 9e37c4c798..e67308d263 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -6,43 +6,61 @@ open Pp
 open Names
 open Term
 open Univ
+open Evd
+open Sign
+open Constant
+open Inductive
 open Environ
-open Machops
+open Typeops
 (*i*)
 
-(*s Machines without information. *)
+(*s Safe environments. *)
 
-val safe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
-val safe_machine_type : 'a unsafe_env -> constr -> typed_type
+type 'a environment
 
-val fix_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
-val fix_machine_type : 'a unsafe_env -> constr -> typed_type
+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 unsafe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
-val unsafe_machine_type : 'a unsafe_env -> constr -> typed_type
+val push_var : identifier * typed_type -> 'a environment -> 'a environment
+val push_rel : name * typed_type -> 'a environment -> 'a environment
+val add_constant : 
+  section_path -> constant_entry -> 'a environment -> 'a environment
+val add_parameter :
+  section_path -> constr -> 'a environment -> 'a environment
+val add_mind : 
+  section_path -> mutual_inductive_entry -> 'a environment -> 'a environment
 
-val type_of : 'a unsafe_env -> constr -> constr
+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 type_of_type : 'a unsafe_env -> constr -> constr
+(*s Typing without information. *)
 
-val unsafe_type_of : 'a unsafe_env -> constr -> constr
+type judgment
 
+val safe_machine : 'a environment -> constr -> judgment * universes
+val safe_machine_type : 'a environment -> constr -> typed_type
 
-(*s Machine with information. *)
+val fix_machine : 'a environment -> constr -> judgment * universes
+val fix_machine_type : 'a environment -> constr -> typed_type
 
-type information = Logic | Inf of unsafe_judgment
+val unsafe_machine : 'a environment -> constr -> judgment * universes
+val unsafe_machine_type : 'a environment -> constr -> typed_type
 
-(*i
-val infexemeta : 
-  'a unsafe_env -> constr -> unsafe_judgment * information * universes
+val type_of : 'a environment -> constr -> constr
 
-val infexecute_type : 
-  'a unsafe_env -> constr -> typed_type * information * universes
+val type_of_type : 'a environment -> constr -> constr
 
-val infexecute : 
-  'a unsafe_env -> constr -> unsafe_judgment * information * universes
+val unsafe_type_of : 'a environment -> constr -> constr
+
+
+(*s Typing with information (extraction). *)
+
+type information = Logic | Inf of judgment
 
-val inf_env_of_env : 'a unsafe_env -> 'a unsafe_env
 
-val core_infmachine : 'a unsafe_env -> constr -> information
-i*)
diff --git a/lib/coqast.mli b/lib/coqast.mli
index 5c7453412e..006b98b3e0 100644
--- a/lib/coqast.mli
+++ b/lib/coqast.mli
@@ -1,5 +1,5 @@
 
-(* $Id$^*)
+(* $Id$ *)
 
 type loc = int * int