- Typing -> Safe_typing

 - proofs/Typing_ev -> pretyping/Typing
 - env -> sign
 - fonctions var_context


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

37 files changed, 378 insertions, 323 deletions

diff --git a/.depend b/.depend
index 0a04467eae..c2d69989d9 100644
--- a/.depend
+++ b/.depend
@@ -18,6 +18,9 @@ kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.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 
+kernel/safe_typing.cmi: kernel/constant.cmi kernel/environ.cmi \
+    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
 kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi 
 kernel/sosub.cmi: kernel/term.cmi 
 kernel/term.cmi: kernel/generic.cmi kernel/names.cmi lib/pp.cmi \
@@ -26,9 +29,6 @@ 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/evd.cmi kernel/names.cmi \
     kernel/term.cmi kernel/univ.cmi 
-kernel/typing.cmi: kernel/constant.cmi kernel/environ.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/pp.cmi 
 lib/gmapl.cmi: lib/gmap.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
@@ -36,8 +36,8 @@ lib/util.cmi: lib/pp.cmi
 library/declare.cmi: kernel/constant.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
-    kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/typing.cmi kernel/univ.cmi 
+    kernel/inductive.cmi kernel/names.cmi kernel/safe_typing.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 library/goptions.cmi: kernel/names.cmi 
 library/impargs.cmi: kernel/names.cmi kernel/term.cmi 
 library/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
@@ -89,6 +89,7 @@ pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     kernel/term.cmi 
 pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
+pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
     kernel/term.cmi lib/util.cmi 
 proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
@@ -105,12 +106,12 @@ proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
 proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/tacinterp.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/tacmach.cmi kernel/term.cmi 
-proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \
-    kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
-    proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi 
+proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \
+    proofs/evar_refiner.cmi kernel/names.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi \
+    kernel/term.cmi 
 proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/reduction.cmi kernel/term.cmi 
-proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/names.cmi \
     proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
     lib/util.cmi 
@@ -206,6 +207,16 @@ kernel/reduction.cmx: kernel/closure.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/term.cmx \
     kernel/univ.cmx lib/util.cmx kernel/reduction.cmi 
+kernel/safe_typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi kernel/indtypes.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/safe_typing.cmi 
+kernel/safe_typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/indtypes.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/safe_typing.cmi 
 kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \
     lib/util.cmi kernel/sign.cmi 
 kernel/sign.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \
@@ -232,16 +243,6 @@ kernel/typeops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.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/evd.cmi \
-    kernel/generic.cmi kernel/indtypes.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/evd.cmx \
-    kernel/generic.cmx kernel/indtypes.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/bij.cmo: lib/gmap.cmi lib/bij.cmi 
@@ -287,12 +288,12 @@ library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
     library/summary.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     library/declare.cmi 
 library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
-    kernel/inductive.cmi kernel/instantiate.cmi kernel/sign.cmi \
-    library/summary.cmi kernel/term.cmi kernel/typing.cmi lib/util.cmi \
+    kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \
+    kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
     library/global.cmi 
 library/global.cmx: kernel/environ.cmx kernel/generic.cmx \
-    kernel/inductive.cmx kernel/instantiate.cmx kernel/sign.cmx \
-    library/summary.cmx kernel/term.cmx kernel/typing.cmx lib/util.cmx \
+    kernel/inductive.cmx kernel/instantiate.cmx kernel/safe_typing.cmx \
+    kernel/sign.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
     library/global.cmi 
 library/goptions.cmo: library/lib.cmi library/libobject.cmi kernel/names.cmi \
     lib/pp.cmi library/summary.cmi lib/util.cmi library/goptions.cmi 
@@ -301,11 +302,11 @@ library/goptions.cmx: library/lib.cmx library/libobject.cmx kernel/names.cmx \
 library/impargs.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi kernel/inductive.cmi kernel/names.cmi \
     kernel/reduction.cmi library/summary.cmi kernel/term.cmi \
-    kernel/typing.cmi library/impargs.cmi 
+    library/impargs.cmi 
 library/impargs.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
     library/global.cmx kernel/inductive.cmx kernel/names.cmx \
     kernel/reduction.cmx library/summary.cmx kernel/term.cmx \
-    kernel/typing.cmx library/impargs.cmi 
+    library/impargs.cmi 
 library/indrec.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
     kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
@@ -410,22 +411,22 @@ pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
     proofs/tacred.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi 
 pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
     pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \
-    pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
+    pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+    kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/coercion.cmi 
 pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
     pretyping/evarconv.cmx kernel/evd.cmx kernel/generic.cmx kernel/names.cmx \
-    pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
+    pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmi \
+    kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/coercion.cmi 
 pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi kernel/generic.cmi kernel/instantiate.cmi \
     kernel/names.cmi pretyping/recordops.cmi kernel/reduction.cmi \
-    kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi pretyping/evarconv.cmi 
+    kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi 
 pretyping/evarconv.cmx: pretyping/classops.cmx kernel/environ.cmx \
     pretyping/evarutil.cmx kernel/generic.cmx kernel/instantiate.cmx \
     kernel/names.cmx pretyping/recordops.cmx kernel/reduction.cmx \
-    kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx pretyping/evarconv.cmi 
+    kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi 
 pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \
@@ -434,8 +435,12 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi 
-pretyping/pretype_errors.cmo: kernel/names.cmi pretyping/pretype_errors.cmi 
-pretyping/pretype_errors.cmx: kernel/names.cmx pretyping/pretype_errors.cmi 
+pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/names.cmi \
+    pretyping/rawterm.cmi kernel/sign.cmi kernel/type_errors.cmi \
+    pretyping/pretype_errors.cmi 
+pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/names.cmx \
+    pretyping/rawterm.cmi kernel/sign.cmx kernel/type_errors.cmx \
+    pretyping/pretype_errors.cmi 
 pretyping/pretyping.cmo: parsing/ast.cmi pretyping/classops.cmi \
     pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \
     pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
@@ -462,32 +467,40 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \
     library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/recordops.cmi 
+pretyping/typing.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
+    kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
+    kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi 
+pretyping/typing.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
+    kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
+    kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi 
 proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/clenv.cmi 
+    pretyping/pretyping.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
+    proofs/clenv.cmi 
 proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/clenv.cmi 
+    pretyping/pretyping.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
+    proofs/clenv.cmi 
 proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \
-    proofs/typing_ev.cmi lib/util.cmi proofs/evar_refiner.cmi 
+    pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi 
 proofs/evar_refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx kernel/term.cmx \
-    proofs/typing_ev.cmx lib/util.cmx proofs/evar_refiner.cmi 
+    pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi 
 proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \
     lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/typeops.cmi kernel/typing.cmi proofs/typing_ev.cmi \
-    lib/util.cmi proofs/logic.cmi 
+    kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi \
+    proofs/logic.cmi 
 proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
     kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx proofs/typing_ev.cmx \
-    lib/util.cmx proofs/logic.cmi 
+    kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx \
+    proofs/logic.cmi 
 proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi library/summary.cmi \
@@ -498,10 +511,10 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
     kernel/term.cmx lib/util.cmx proofs/macros.cmi 
 proofs/proof_trees.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
-    proofs/typing_ev.cmi lib/util.cmi proofs/proof_trees.cmi 
+    pretyping/typing.cmi lib/util.cmi proofs/proof_trees.cmi 
 proofs/proof_trees.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/names.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
-    proofs/typing_ev.cmx lib/util.cmx proofs/proof_trees.cmi 
+    pretyping/typing.cmx lib/util.cmx proofs/proof_trees.cmi 
 proofs/refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
@@ -516,18 +529,18 @@ proofs/tacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi proofs/macros.cmi \
 proofs/tacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx proofs/macros.cmx \
     kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \
     kernel/term.cmx lib/util.cmx proofs/tacinterp.cmi 
-proofs/tacmach.cmo: parsing/ast.cmi kernel/environ.cmi \
+proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \
     kernel/sign.cmi lib/stamps.cmi proofs/tacred.cmi kernel/term.cmi \
-    proofs/typing_ev.cmi lib/util.cmi proofs/tacmach.cmi 
-proofs/tacmach.cmx: parsing/ast.cmx kernel/environ.cmx \
+    pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi 
+proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx kernel/evd.cmx kernel/generic.cmx \
     kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \
     kernel/sign.cmx lib/stamps.cmx proofs/tacred.cmx kernel/term.cmx \
-    proofs/typing_ev.cmx lib/util.cmx proofs/tacmach.cmi 
+    pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi 
 proofs/tacred.cmo: kernel/closure.cmi library/declare.cmi kernel/environ.cmi \
     kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \
     kernel/names.cmi lib/pp.cmi library/redinfo.cmi kernel/reduction.cmi \
@@ -536,12 +549,6 @@ proofs/tacred.cmx: kernel/closure.cmx library/declare.cmx kernel/environ.cmx \
     kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \
     kernel/names.cmx lib/pp.cmx library/redinfo.cmx kernel/reduction.cmx \
     kernel/term.cmx lib/util.cmx proofs/tacred.cmi 
-proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
-    kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
-    kernel/typeops.cmi lib/util.cmi proofs/typing_ev.cmi 
-proofs/typing_ev.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
-    kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
-    kernel/typeops.cmx lib/util.cmx proofs/typing_ev.cmi 
 tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \
     tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
     tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \
@@ -549,7 +556,7 @@ tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \
     tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \
     proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi tactics/auto.cmi 
 tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \
     tactics/dhyp.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
@@ -558,7 +565,7 @@ tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \
     tactics/pattern.cmx proofs/pfedit.cmi lib/pp.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \
     proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx tactics/auto.cmi 
 tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \
     tactics/btermdn.cmi 
@@ -664,12 +671,12 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
 toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
     kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typing.cmi lib/util.cmi 
+    kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/type_errors.cmi lib/util.cmi 
 toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
     kernel/generic.cmx toplevel/himsg.cmx kernel/inductive.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typing.cmx lib/util.cmx 
+    kernel/names.cmx lib/pp.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/type_errors.cmx lib/util.cmx 
 toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
     lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi toplevel/mltop.cmi 
@@ -706,7 +713,7 @@ toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \
     proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \
     library/states.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \
-    kernel/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+    pretyping/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \
     pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \
     kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \
@@ -715,7 +722,7 @@ toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \
     proofs/pfedit.cmi lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \
     library/states.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \
-    kernel/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
+    pretyping/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
     toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \
diff --git a/Makefile b/Makefile
index 64bec2282a..f94270d712 100644
--- a/Makefile
+++ b/Makefile
@@ -42,24 +42,14 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \
        kernel/closure.cmo kernel/reduction.cmo \
        kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
-       kernel/typing.cmo
+       kernel/safe_typing.cmo
 
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
 	library/global.cmo library/states.cmo library/library.cmo \
 	library/nametab.cmo library/impargs.cmo library/redinfo.cmo \
         library/indrec.cmo library/declare.cmo
 
-PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \
-       proofs/proof_trees.cmo proofs/logic.cmo \
-       proofs/refiner.cmo proofs/evar_refiner.cmo \
-       proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo
-
-TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
-        tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \
-	tactics/wcclausenv.cmo tactics/tacticals.cmo \
-        tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
-
-PRETYPING=pretyping/classops.cmo pretyping/recordops.cmo \
+PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.cmo \
           pretyping/evarutil.cmo pretyping/evarconv.cmo \
           pretyping/pretype_errors.cmo pretyping/coercion.cmo \
 	  pretyping/multcase.cmo pretyping/pretyping.cmo
@@ -69,6 +59,16 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\
         parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo
 
+PROOFS=proofs/tacred.cmo \
+       proofs/proof_trees.cmo proofs/logic.cmo \
+       proofs/refiner.cmo proofs/evar_refiner.cmo \
+       proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo
+
+TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
+        tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \
+	tactics/wcclausenv.cmo tactics/tacticals.cmo \
+        tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
+
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
          toplevel/vernac.cmo toplevel/mltop.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
@@ -76,15 +76,15 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
 
-CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PROOFS) $(TACTICS) \
-    $(PRETYPING) $(PARSING) $(TOPLEVEL)
+CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \
+    $(PROOFS) $(TACTICS) $(TOPLEVEL)
 CMX=$(CMO:.cmo=.cmx)
 
 # Targets
 
 world: minicoq coqtop.byte dev/db_printers.cmo
 
-LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY)  $(PARSING) $(PRETYPING)
+LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING) $(PRETYPING)
 # $(PROOFS) $(TACTICS) $(TOPLEVEL)
 link: $(LINK)
 	ocamlc -o link $(LINK)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ccf3e1e20c..bed45797d8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,6 +43,7 @@ let empty_env = {
 
 let universes env = env.env_universes
 let context env = env.env_context
+let var_context env = let (ENVIRON(g,_)) = env.env_context in g
 
 (* Construction functions. *)
 
@@ -50,8 +51,8 @@ let push_var idvar env =
   { env with env_context = add_glob idvar env.env_context }
 
 let change_hyps f env =
-  let ctx = env.env_context in
-  { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) }
+  let (ENVIRON(g,r)) = env.env_context in
+  { env with env_context = ENVIRON (f g, r) }
 
 let push_rel idrel env =
   { env with env_context = add_rel idrel env.env_context }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d3fd22c01e..9f1c228a00 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -22,6 +22,7 @@ val empty_env : unsafe_env
 
 val universes : unsafe_env -> universes
 val context : unsafe_env -> context
+val var_context : unsafe_env -> var_context
 
 val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
 val change_hyps : 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index dd387ddfb4..4599fbdc43 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -65,7 +65,7 @@ let is_defined sigma ev =
   let info = map sigma ev in 
   not (info.evar_body = Evar_empty)
 
-let evar_hyps ev = get_globals (context ev.evar_env)
+let evar_hyps ev = var_context ev.evar_env
 
 let id_of_existential ev =
   id_of_string ("?" ^ string_of_int ev)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 96fe8d5846..00e8a442bb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -244,7 +244,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
   let packets = Array.of_list (list_map_i one_packet 1 inds) in
   { mind_kind = kind;
     mind_ntypes = ntypes;
-    mind_hyps = get_globals (context env);
+    mind_hyps = var_context env;
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None;
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4bc551c6aa..2ce121ed12 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma
 (* 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 sigma = function
+let rec whd_ise1_metas sigma = function
   | (DOPN(Evar n,_) as k) ->
       if Evd.in_dom sigma n then
 	if Evd.is_defined sigma n then
-      	  whd_ise1_metas env sigma (existential_value sigma k)
+      	  whd_ise1_metas sigma (existential_value sigma k)
 	else 
       	  let m = DOP0(Meta (new_meta())) in
 	  DOP2(Cast,m,existential_type sigma k)
       else
 	k
-  | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c
+  | DOP2(Cast,c,_) -> whd_ise1_metas sigma c
   | c -> c
 
 
diff --git a/kernel/typing.ml b/kernel/safe_typing.ml
index db3d00302e..e523be5108 100644
--- a/kernel/typing.ml
+++ b/kernel/safe_typing.ml
@@ -233,6 +233,7 @@ let empty_environment = empty_env
 
 let universes = universes
 let context = context
+let var_context = var_context
 
 let lookup_var = lookup_var
 let lookup_rel = lookup_rel
@@ -283,7 +284,7 @@ let add_constant sp ce env =
     const_kind = kind_of_path sp;
     const_body = Some ce.const_entry_body;
     const_type = ty;
-    const_hyps = get_globals (context env);
+    const_hyps = var_context env;
     const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
@@ -296,7 +297,7 @@ let add_parameter sp t env =
     const_kind = kind_of_path sp;
     const_body = None;
     const_type = assumption_of_judgment env' Evd.empty jt;
-    const_hyps = get_globals (context env);
+    const_hyps = var_context env;
     const_constraints = cst;
     const_opaque = false } 
   in
diff --git a/kernel/typing.mli b/kernel/safe_typing.mli
index 10530d123b..392040814f 100644
--- a/kernel/typing.mli
+++ b/kernel/safe_typing.mli
@@ -24,6 +24,7 @@ val empty_environment : environment
 
 val universes : environment -> universes
 val context : environment -> context
+val var_context : environment -> var_context
 
 val push_var : identifier * constr -> environment -> environment
 val push_rel : name * constr -> environment -> environment
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 5d7d5309b0..0b34c7edf3 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -10,7 +10,7 @@ open Term
 
 type 'a signature = identifier list * 'a list
 type 'a db_signature = (name * 'a) list
-type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
+type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
 
 let gLOB hyps = ENVIRON (hyps,[])
 
@@ -233,7 +233,7 @@ let lookup_id id env =
     | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
 
 
-type 'b assumptions = (typed_type,'b) env
-type context = (typed_type,typed_type) env
+type 'b assumptions = (typed_type,'b) sign
+type context = (typed_type,typed_type) sign
 type var_context = typed_type signature
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 2a0a567dec..e2ef7d4a1e 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term
 (*s Signatures with named and de Bruijn variables. *)
 
 type 'a db_signature = (name * 'a) list
-type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
-
-val gLOB : 'b signature -> ('b,'a) env
-
-val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env 
-val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env
-val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b)
-val lookup_rel : int -> ('b,'a) env  -> (name * 'a)
-val mem_glob : identifier -> ('b,'a) env -> bool
-
-val get_globals : ('b,'a) env -> 'b signature
-val get_rels : ('b,'a) env -> 'a db_signature
-val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c
-val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c
-val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env
-val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env
-val isnull_rel_env : ('a,'b) env -> bool
-val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env
-val ids_of_env : ('a, 'b) env -> identifier list
+type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
+
+val gLOB : 'b signature -> ('b,'a) sign
+
+val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign 
+val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign
+val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
+val lookup_rel : int -> ('b,'a) sign  -> (name * 'a)
+val mem_glob : identifier -> ('b,'a) sign -> bool
+
+val get_globals : ('b,'a) sign -> 'b signature
+val get_rels : ('b,'a) sign -> 'a db_signature
+val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
+val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c
+val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign
+val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
+val isnull_rel_env : ('a,'b) sign -> bool
+val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
+val ids_of_env : ('a, 'b) sign -> identifier list
 
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
   | RELNAME of int * 'a
 
-val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
+val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result
 
 
-type 'b assumptions = (typed_type,'b) env
-type context = (typed_type,typed_type) env
+type 'b assumptions = (typed_type,'b) sign
+type context = (typed_type,typed_type) sign
 type var_context = typed_type signature
 
 val unitize_env : 'a assumptions -> unit assumptions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index d224b0209e..0d2d5cba50 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -75,14 +75,14 @@ let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) =
    current context of [env]. *)
 
 let construct_reference id env sigma hyps =
-  let hyps' = get_globals (context env) in
+  let hyps' = var_context env in
   if hyps_inclusion env sigma hyps hyps' then
     Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))
   else 
     error_reference_variables CCI env id
 
 let check_hyps id env sigma hyps =
-  let hyps' = get_globals (context env) in
+  let hyps' = var_context env in
   if not (hyps_inclusion env sigma hyps hyps') then
     error_reference_variables CCI env id
 
@@ -178,7 +178,7 @@ let type_inst_construct env sigma i mind =
 let type_of_existential env sigma c =
   let (ev,args) = destEvar c in
   let evi = Evd.map sigma ev in
-  let hyps = get_globals (context evi.Evd.evar_env) in
+  let hyps = var_context evi.Evd.evar_env in
   let id = id_of_string ("?" ^ string_of_int ev) in
   check_hyps id env sigma hyps;
   instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
diff --git a/library/declare.ml b/library/declare.ml
index 5d7d624121..0dcdf3dd28 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -213,7 +213,7 @@ let global_operator sp id =
 let global_reference kind id =
   let sp = Nametab.sp_of_id kind id in
   let (oper,_) = global_operator sp id in
-  let hyps = get_globals (Global.context ()) in
+  let hyps = Global.var_context () in
   let ids = ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
diff --git a/library/global.ml b/library/global.ml
index 9238b6e85c..0fc1852cb9 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@ open Generic
 open Term
 open Instantiate
 open Sign
-open Typing
+open Safe_typing
 open Summary
 
 (* We introduce here the global environment of the system, and we declare it
@@ -28,6 +28,7 @@ let _ =
 
 let universes () = universes !global_env
 let context () = context !global_env
+let var_context () = var_context !global_env
 
 let push_var idc = global_env := push_var idc !global_env
 let push_rel nac = global_env := push_rel nac !global_env
diff --git a/library/global.mli b/library/global.mli
index 22623424bb..3e557b350b 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -9,7 +9,7 @@ open Sign
 open Constant
 open Inductive
 open Environ
-open Typing
+open Safe_typing
 (*i*)
 
 (* This module defines the global environment of Coq. 
@@ -21,6 +21,7 @@ val unsafe_env : unit -> unsafe_env
 
 val universes : unit -> universes
 val context : unit -> context
+val var_context : unit -> var_context
 
 val push_var : identifier * constr -> unit
 val push_rel : name * constr -> unit
diff --git a/library/impargs.ml b/library/impargs.ml
index a8fe59cc80..8fe93b97c1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -7,7 +7,6 @@ open Term
 open Reduction
 open Constant
 open Inductive
-open Typing
 
 type implicits =
   | Impl_auto of int list
@@ -18,7 +17,7 @@ let implicit_args = ref false
 
 let auto_implicits ty =
   if !implicit_args then
-    let genv = unsafe_env_of_env (Global.env()) in
+    let genv = Global.unsafe_env() in
     Impl_auto (poly_args genv Evd.empty ty)
   else
     No_impl
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index fddb478045..f2befc1d26 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -615,7 +615,7 @@ let ast_adjust_consts sigma = (* locations are kept *)
 
 let globalize_command ast =
   let env = Global.unsafe_env () in
-  let sign = get_globals (Environ.context env) in
+  let sign = Environ.var_context env in
   ast_adjust_consts Evd.empty (gLOB sign) ast
 
 (* Avoid globalizing in non command ast for tactics *)
@@ -633,8 +633,7 @@ let rec glob_ast sigma env = function
   | x -> x
 
 let globalize_ast ast =
-  let env = Global.unsafe_env () in
-  let sign = get_globals (Environ.context env) in
+  let sign = Global.var_context () in
   glob_ast Evd.empty (gLOB sign) ast
 
 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 0588446225..ea83e68b1f 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -42,7 +42,7 @@ let print_basename_mind sp mindid =
 let print_closed_sections = ref false
 
 let print_typed_value_in_env env (trm,typ) =
-  let sign = get_globals (Environ.context env) in
+  let sign = Environ.var_context env in
   [< term0 (gLOB sign) trm ; 'fNL ;
      'sTR "     : "; term0 (gLOB sign) typ ; 'fNL >]
 
@@ -352,7 +352,7 @@ let print_constructors_rel fn mip =
   List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid
 
 let crible (fn:string -> unit assumptions -> constr -> unit) name =
-  let hyps = gLOB (get_globals (Global.context())) in
+  let hyps = gLOB (Global.var_context()) in
   let imported = Library.opened_modules() in
   let const = global_reference CCI name in 
   let rec crible_rec = function
@@ -438,7 +438,7 @@ let print_name name =
 let print_opaque_name name = 
   let sigma = Evd.empty in
   let env = Global.unsafe_env () in
-  let sign = get_globals (Global.context ()) in
+  let sign = Global.var_context () in
   try 
     match global_reference CCI name with
       | DOPN(Const sp,_) as x ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7959b5c7c2..f7096f2682 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,64 +1,77 @@
 
 (* $Id$ *)
 
-open Util;;
-open Generic;;
-open Names;;
-open Term;;
-open Reduction;;
-open Environ;;
-open Typeops;;
-open Type_errors;;
-open Classops;;
-open Recordops;;
-open Evarconv;;
+open Util
+open Generic
+open Names
+open Term
+open Reduction
+open Environ
+open Typeops
+open Type_errors
+open Classops
+open Recordops
+open Evarconv
+open Retyping
 
 (* Typing operations dealing with coercions *)
 
-let class_of1 env sigma t = class_of sigma (nf_ise1 env sigma t);;
+let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t)
 
 let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} =
-  {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k}
+  { uj_val = nf_ise1 sigma v; 
+    uj_type = nf_ise1 sigma t; 
+    uj_kind = k }
+
 let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
 
 (* Here, funj is a coercion therefore already typed in global context *)
 let apply_coercion_args env argl funj =
   let rec apply_rec acc typ = function
-      [] -> {uj_val=applist(j_val_only funj,argl);
-             uj_type= typ;
-             uj_kind = funj.uj_kind}
+    | [] -> { uj_val=applist(j_val_only funj,argl);
+              uj_type= typ;
+              uj_kind = funj.uj_kind }
     | h::restl ->
- (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
-  match whd_betadeltaiota env Evd.empty typ with
-     DOP2(Prod,c1,DLAM(_,c2)) -> (* Typage garanti par l'appel a app_coercion*)
-       apply_rec (h::acc) (subst1 h c2) restl
-    | _ -> anomaly "apply_coercion_args"
-  in apply_rec [] funj.uj_type argl;;
+      (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
+  	match whd_betadeltaiota env Evd.empty typ with
+	  | DOP2(Prod,c1,DLAM(_,c2)) -> 
+              (* Typage garanti par l'appel a app_coercion*)
+	      apply_rec (h::acc) (subst1 h c2) restl
+	  | _ -> anomaly "apply_coercion_args"
+  in 
+  apply_rec [] funj.uj_type argl
 
 (* appliquer le chemin de coercions p a` hj *)
 
 let apply_pcoercion env p hj typ_cl =
-  if !compter then
-    (nbpathc := !nbpathc +1; nbcoer := !nbcoer + (List.length p));
-  try fst (List.fold_left
-             (fun (ja,typ_cl) i -> 
-                let fv,b= coe_value i in
-                let argl = (class_args_of typ_cl)@[ja.uj_val] in
-                let jres = apply_coercion_args env argl fv in
-                  (if b then {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val}
-                   else jres),jres.uj_type)
-             (hj,typ_cl) p)
-  with _ -> failwith "apply_pcoercion"
+  if !compter then begin
+    nbpathc := !nbpathc +1; 
+    nbcoer := !nbcoer + (List.length p)
+  end;
+  try 
+    fst (List.fold_left
+           (fun (ja,typ_cl) i -> 
+              let fv,b= coe_value i in
+              let argl = (class_args_of typ_cl)@[ja.uj_val] in
+              let jres = apply_coercion_args env argl fv in
+              (if b then 
+		 {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val}
+               else 
+		 jres),
+	      jres.uj_type)
+           (hj,typ_cl) p)
+  with _ -> 
+    failwith "apply_pcoercion"
 
 let inh_app_fun env isevars j = 
- match whd_betadeltaiota env !isevars j.uj_type with
-    DOP2(Prod,_,DLAM(_,_)) -> j
-   | _ ->
-       (try
- 	let t,i1 = class_of1 env !isevars j.uj_type in
-      	let p = lookup_path_to_fun_from i1 in
-        apply_pcoercion env p j t
-      with _ -> j)
+  match whd_betadeltaiota env !isevars j.uj_type with
+    | DOP2(Prod,_,DLAM(_,_)) -> j
+    | _ ->
+       	(try
+ 	   let t,i1 = class_of1 env !isevars j.uj_type in
+      	   let p = lookup_path_to_fun_from i1 in
+           apply_pcoercion env p j t
+	 with _ -> j)
 (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *)
 
 let inh_tosort_force env isevars j =
@@ -69,110 +82,126 @@ let inh_tosort_force env isevars j =
 let inh_tosort env isevars j = 
   let typ = whd_betadeltaiota env !isevars j.uj_type in
   match typ with
-    DOP0(Sort(_)) -> j  (* idem inh_app_fun *)
-  | _ -> (try inh_tosort_force env isevars j with _ -> j)
+    | DOP0(Sort(_)) -> j  (* idem inh_app_fun *)
+    | _ -> (try inh_tosort_force env isevars j with _ -> j)
 
 let inh_ass_of_j env isevars j =
-   let typ = whd_betadeltaiota env !isevars j.uj_type in
-     match typ with
-         DOP0(Sort s) -> {body=j.uj_val;typ=s}
-       | _ ->
-           (try
-             let j1 = inh_tosort_force env isevars j
-             in assumption_of_judgment env !isevars j1 
-           with _ -> error_assumption CCI env (nf_ise1 env !isevars j.uj_val))
-                   (* try ... with _ -> ... is BAD *)
+  let typ = whd_betadeltaiota env !isevars j.uj_type in
+  match typ with
+    | DOP0(Sort s) -> {body=j.uj_val;typ=s}
+    | _ ->
+        (try
+           let j1 = inh_tosort_force env isevars j in 
+	   assumption_of_judgment env !isevars j1 
+         with _ -> 
+	   error_assumption CCI env (nf_ise1 !isevars j.uj_val))
+           (* try ... with _ -> ... is BAD *)
 
 let inh_coerce_to1 env isevars c1 v t k =
- let t1,i1 = class_of1 env !isevars c1 in
- let t2,i2 = class_of1 env !isevars t in
- let p = lookup_path_between (i2,i1) in
- let hj = {uj_val=v;uj_type=t;uj_kind=k} in
- let hj' = apply_pcoercion env p hj t2 in
- if the_conv_x_leq env isevars hj'.uj_type c1 then hj'
- else failwith "inh_coerce_to"
+  let t1,i1 = class_of1 env !isevars c1 in
+  let t2,i2 = class_of1 env !isevars t in
+  let p = lookup_path_between (i2,i1) in
+  let hj = {uj_val=v;uj_type=t;uj_kind=k} in
+  let hj' = apply_pcoercion env p hj t2 in
+  if the_conv_x_leq env isevars hj'.uj_type c1 then 
+    hj'
+  else 
+    failwith "inh_coerce_to"
 
 let inh_coerce_to env isevars c1 hj =
   inh_coerce_to1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind
-
+    
 let rec inh_conv_coerce1 env isevars c1 v t k =
- if the_conv_x_leq env isevars t c1 
- then {uj_val=v; uj_type=t; uj_kind=k}
- else try inh_coerce_to1 env isevars c1 v t k
- with _ ->  (* try ... with _ -> ... is BAD *)
-
-(*   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
-   (match (whd_betadeltaiota env !isevars t,
-	   whd_betadeltaiota env !isevars c1) with
-      | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> 
-(*          let v' = hnf_constr !isevars v in*)
-          let v' = whd_betadeltaiota env !isevars v in
-            if (match v' with
-                    DOP2(Lambda,v1,DLAM(_,v2)) ->
-                      the_conv_x env isevars v1 u1 (* leq v1 u1? *)
-                  |         _                -> false)
-            then 
-	      let (x,v1,v2) = destLambda v' in
-(*              let jv1 = exemeta_rec def_vty_con env isevars v1 in 
-	      let assv1 = assumption_of_judgement env !isevars jv1 in
- *)
-	      let assv1 = outcast_type v1 in
-              let env1 = push_rel (x,assv1) env in
-              let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 (mkSort (sort_of env !isevars1 t2)) in
-              abs_rel !isevars x assv1 h2
-            else 
-(*
-	      let ju1 = exemeta_rec def_vty_con env isevars u1 in 
-              let assu1 = assumption_of_judgement env !isevars ju1 in
- *)
-	      let assu1 = outcast_type u1 in
-              let name = (match name with Anonymous -> Name (id_of_string "x")
-                            | _ -> name) in
-              let env1 = add_rel (name,assu1) env in
-              let h1 = 
-		inh_conv_coerce1 env isevars1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in
-              let h2 = inh_conv_coerce1 env isevars1 u2  
-			 (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) 
-                         (subst1 h1.uj_val t2) 
-			 (mkSort (sort_of env !isevars1 t2)) in
-	      abs_rel !isevars name assu1 h2
-      | _ -> failwith "inh_coerce_to")
+  if the_conv_x_leq env isevars t c1 then 
+    {uj_val=v; uj_type=t; uj_kind=k}
+  else 
+    try 
+      inh_coerce_to1 env isevars c1 v t k
+    with _ ->  (* try ... with _ -> ... is BAD *)
+      (*   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
+      (match (whd_betadeltaiota env !isevars t,
+	      whd_betadeltaiota env !isevars c1) with
+	 | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> 
+ 	     (* let v' = hnf_constr !isevars v in *)
+             let v' = whd_betadeltaiota env !isevars v in
+             if (match v' with
+                   | DOP2(Lambda,v1,DLAM(_,v2)) ->
+                       the_conv_x env isevars v1 u1 (* leq v1 u1? *)
+                   | _  -> false)
+             then 
+	       let (x,v1,v2) = destLambda v' in
+               (* let jv1 = exemeta_rec def_vty_con env isevars v1 in 
+	          let assv1 = assumption_of_judgement env !isevars jv1 in *)
+	       let assv1 = outcast_type v1 in
+               let env1 = push_rel (x,assv1) env in
+               let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 
+			  (mkSort (get_sort_of env !isevars t2)) in
+               abs_rel env !isevars x assv1 h2
+             else 
+               (* let ju1 = exemeta_rec def_vty_con env isevars u1 in 
+		  let assu1 = assumption_of_judgement env !isevars ju1 in *)
+	       let assu1 = outcast_type u1 in
+               let name = (match name with 
+			     | Anonymous -> Name (id_of_string "x")
+                             | _ -> name) in
+               let env1 = push_rel (name,assu1) env in
+               let h1 = 
+		 inh_conv_coerce1 env isevars t1 (Rel 1) u1 
+		   (mkSort (level_of_type assu1)) in
+               let h2 = inh_conv_coerce1 env isevars1 u2  
+			  (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) 
+                          (subst1 h1.uj_val t2) 
+			  (mkSort (sort_of env !isevars1 t2)) 
+	       in
+	       abs_rel !isevars name assu1 h2
+	 | _ -> failwith "inh_coerce_to")
             
 let inh_conv_coerce env isevars c1 hj =
   inh_conv_coerce1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind
 
 let inh_cast_rel env isevars cj tj =
-    let cj' = (try inh_conv_coerce env isevars tj.uj_val cj 
-              with Not_found | Failure _ -> error_actual_type CCI env 
-		  (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)) in
-      { uj_val = mkCast cj'.uj_val tj.uj_val;
-        uj_type = tj.uj_val;
-        uj_kind = whd_betadeltaiota env !isevars tj.uj_type}
+  let cj' = 
+    try 
+      inh_conv_coerce env isevars tj.uj_val cj 
+    with Not_found | Failure _ -> 
+      error_actual_type CCI env 
+	(j_nf_ise !isevars cj) (j_nf_ise !isevars tj) 
+  in
+  { uj_val = mkCast cj'.uj_val tj.uj_val;
+    uj_type = tj.uj_val;
+    uj_kind = whd_betadeltaiota env !isevars tj.uj_type }
 
 let inh_apply_rel_list nocheck env isevars argjl funj vtcon =
   let rec apply_rec acc typ = function
-    [] -> let resj =
-      {uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc));
-       uj_type= typ;
-       uj_kind = funj.uj_kind} in
-      (match vtcon with 
-      | (_,(_,Some typ')) ->
-          (try inh_conv_coerce env isevars typ' resj
-          with _ -> resj) (* try ... with _ -> ... is BAD *)
-      | (_,(_,None)) -> resj)
-
-  | hj::restjl ->
-      match whd_betadeltaiota env !isevars typ with
-          DOP2(Prod,c1,DLAM(_,c2)) ->
-            let hj' =
-              if nocheck then hj else 
-	      (try inh_conv_coerce env isevars c1 hj 
-               with (Failure _ | Not_found) ->
-                 error_cant_apply "Type Error" CCI env
-		   (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) in
-            apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl
-        | _ ->
-            error_cant_apply "Non-functional construction" CCI env
-	      (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)
-  in apply_rec [] funj.uj_type argjl
-;;
+    | [] -> 
+	let resj =
+      	  { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc));
+	    uj_type= typ;
+	    uj_kind = funj.uj_kind } 
+      	in
+      	(match vtcon with 
+	   | (_,(_,Some typ')) ->
+               (try inh_conv_coerce env isevars typ' resj
+          	with _ -> resj) (* try ... with _ -> ... is BAD *)
+	   | (_,(_,None)) -> resj)
+
+    | hj::restjl ->
+      	match whd_betadeltaiota env !isevars typ with
+          | DOP2(Prod,c1,DLAM(_,c2)) ->
+              let hj' =
+              	if nocheck then 
+		  hj 
+		else 
+		  (try 
+		     inh_conv_coerce env isevars c1 hj 
+		   with Failure _ | Not_found ->
+                     error_cant_apply "Type Error" CCI env
+		       (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) 
+	      in
+              apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl
+          | _ ->
+              error_cant_apply "Non-functional construction" CCI env
+	      	(j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)
+  in 
+  apply_rec [] funj.uj_type argjl
+
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cd9e6d9211..5af5fb9156 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -8,7 +8,7 @@ open Term
 open Reduction
 open Instantiate
 open Environ
-open Typing_ev
+open Typing
 open Classops
 open Recordops 
 open Evarutil
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 43653f80d4..226b6ff0de 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -45,7 +45,7 @@ let filter_sign p sign x =
 
 (* All ids of sign must be distincts! *)
 let new_isevar_sign env sigma typ args =
-  let sign = get_globals (context env) in
+  let sign = var_context env in
   if not (list_distinct (ids_of_sign sign)) then 
     error "new_isevar_sign: two vars have the same name";
   let newev = Evd.new_evar() in
@@ -60,7 +60,7 @@ let dummy_sort = mkType dummy_univ
 (* Declaring any type to be in the sort Type shouldn't be harmful since
    cumulativity now includes Prop and Set in Type. *)
 let new_type_var env sigma =
-  let sign = get_globals (context env) in
+  let sign = var_context env in
   let args = (Array.of_list (List.map mkVar (ids_of_sign sign))) in
   let (sigma',c) = new_isevar_sign env sigma dummy_sort args in
   (sigma', make_typed c (Type dummy_univ))
@@ -70,7 +70,7 @@ let split_evar_to_arrow sigma c =
   let evd = Evd.map sigma ev in
   let evenv = evd.evar_env in
   let (sigma1,dom) = new_type_var evenv sigma in
-  let hyps = get_globals (context evenv) in
+  let hyps = var_context evenv in
   let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in
   let nevenv = push_var (nvar,dom) evenv in
   let (sigma2,rng) = new_type_var nevenv sigma1 in
@@ -97,7 +97,7 @@ let do_restrict_hyps sigma c =
   let args = Array.to_list args in
   let evd = Evd.map sigma ev in
   let env = evd.evar_env in
-  let hyps = get_globals (context env) in
+  let hyps = var_context env in
   let (_,(rsign,ncargs)) =
     List.fold_left 
       (fun (sign,(rs,na)) a ->
@@ -244,7 +244,7 @@ let evar_define isevars lhs rhs =
   let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
       (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
-  let hyps = get_globals (context evd.evar_env) in
+  let hyps = var_context evd.evar_env in
   (* the substitution to invert *)
   let worklist = List.combine (ids_of_sign hyps) args in
   let body = real_clean isevars ev worklist rhs in
@@ -263,7 +263,7 @@ let solve_refl conv_algo isevars c1 c2 =
   and (_,argsv2) = destEvar c2 in
   let evd = Evd.map !isevars ev in
   let env = evd.evar_env in
-  let hyps = get_globals (context env) in
+  let hyps = var_context env in
   let (_,rsign) = 
     array_fold_left2
       (fun (sgn,rsgn) a1 a2 ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1e6245a471..500e6bfe74 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -146,17 +146,17 @@ let mt_evd = Evd.empty
 
 let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
 
-let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} =
-  {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k}
+let j_nf_ise sigma {uj_val=v;uj_type=t;uj_kind=k} =
+  {uj_val=nf_ise1 sigma v;uj_type=nf_ise1 sigma t;uj_kind=k}
 
-let jv_nf_ise env sigma = Array.map (j_nf_ise env sigma)
+let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
 
 (* Utilisé pour inférer le prédicat des Cases *)
 (* Semble exagérement fort *)
 (* Faudra préférer une unification entre les types de toutes les clauses *)
 (* et autoriser des ? à rester dans le résultat de l'unification *)
-let has_ise env sigma t = 
-  try let _ = whd_ise env sigma t in true
+let has_ise sigma t = 
+  try let _ = whd_ise sigma t in true
   with UserError _ -> false
 
 let evar_type_fixpoint env isevars lna lar vdefj =
@@ -166,8 +166,8 @@ let evar_type_fixpoint env isevars lna lar vdefj =
         if not (the_conv_x_leq env isevars
 		  (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then
           error_ill_typed_rec_body CCI env i lna 
-	    (jv_nf_ise env !isevars vdefj) 
-	    (Array.map (typed_app (nf_ise1 env !isevars)) lar)
+	    (jv_nf_ise !isevars vdefj) 
+	    (Array.map (typed_app (nf_ise1 !isevars)) lar)
       done
 
 
@@ -183,7 +183,7 @@ let cast_rel isevars env cj tj =
 let let_path = make_path ["Core"] (id_of_string "let") CCI
 
 let wrong_number_of_cases_message loc env isevars (c,ct) expn = 
-  let c = nf_ise1 env !isevars c and ct = nf_ise1 env !isevars ct in
+  let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in
   error_number_branches_loc loc CCI env c ct expn
 
 let check_branches_message loc env isevars (c,ct) (explft,lft) = 
@@ -191,10 +191,11 @@ let check_branches_message loc env isevars (c,ct) (explft,lft) =
   if n<>expn then wrong_number_of_cases_message loc env isevars (c,ct) expn;
   for i = 0 to n-1 do
     if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
-      let c = nf_ise1 env !isevars c
-      and ct = nf_ise1 env !isevars ct 
-      and lfi = nf_betaiota env !isevars (nf_ise1 env !isevars lft.(i)) in
-      error_ill_formed_branch_loc loc CCI env c i lfi (nf_betaiota env !isevars explft.(i))
+      let c = nf_ise1 !isevars c
+      and ct = nf_ise1 !isevars ct 
+      and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in
+      error_ill_formed_branch_loc loc CCI env c i lfi 
+	(nf_betaiota env !isevars explft.(i))
   done
 
 (*
@@ -287,10 +288,10 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       let (valc,typc) = destCast v in
       {uj_val=valc; uj_type=typc; uj_kind=dummy_sort}
   | (false,(None,Some ty)) ->
-      let (c,ty) = new_isevar env isevars ty CCI in
+      let (c,ty) = new_isevar isevars env ty CCI in
       {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
   | (true,(None,None)) ->
-      let (c,ty) = new_isevar env isevars (mkCast dummy_sort dummy_sort) CCI in
+      let (c,ty) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in
       {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
   | (false,(None,None)) ->
       (match loc with
@@ -336,19 +337,20 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     let j = pretype mt_tycon env isevars f in
     let j = inh_app_fun env isevars j in
     let apply_one_arg (tycon,jl) c =
-      let cj = pretype (app_dom_tycon isevars tycon) env isevars c in
-      let rtc = app_rng_tycon isevars cj.uj_val tycon in
+      let cj = pretype (app_dom_tycon env isevars tycon) env isevars c in
+      let rtc = app_rng_tycon env isevars cj.uj_val tycon in
       (rtc,cj::jl)  in
     let jl = List.rev (snd (List.fold_left apply_one_arg
 			      (mk_tycon j.uj_type,[]) args)) in
     inh_apply_rel_list !trad_nocheck env isevars jl j vtcon
 
 | RBinder(loc,BLambda,name,c1,c2)      ->
-    let j = pretype (abs_dom_valcon isevars vtcon) env isevars c1 in
+    let j = pretype (abs_dom_valcon env isevars vtcon) env isevars c1 in
     let assum = inh_ass_of_j env isevars j in
     let var = (name,assum) in
     let j' =
-      pretype (abs_rng_tycon isevars vtcon) (push_rel var env) isevars c2 in 
+      pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars c2 
+    in 
     fst (abs_rel env !isevars name assum j')
 
 | RBinder(loc,BProd,name,c1,c2)        ->
@@ -364,7 +366,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
   let (mind,_) =
     try find_mrectype env !isevars cj.uj_type
     with Induc -> error_case_not_inductive CCI env
-	(nf_ise1 env !isevars cj.uj_val) (nf_ise1 env !isevars cj.uj_type) in
+	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
   let pj = match po with
     | Some p -> pretype mt_tycon env isevars p
     | None -> 
@@ -382,11 +384,11 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	      try
 		let expti = Indrec.branch_scheme env !isevars isrec i cj.uj_type in
 		let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in
-		let efjt = nf_ise1 env !isevars fj.uj_type in 
+		let efjt = nf_ise1 !isevars fj.uj_type in 
 		let pred = 
 		  Indrec.pred_case_ml_onebranch env !isevars isrec 
 		    (cj.uj_val,cj.uj_type) (i,fj.uj_val,efjt) in
-		if has_ise env !isevars pred then findtype (i+1)
+		if has_ise !isevars pred then findtype (i+1)
 		else 
 		  let pty = Retyping.get_type_of env !isevars pred in
 		  let k = Retyping.get_type_of env !isevars pty in
@@ -394,8 +396,8 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	      with UserError _ -> findtype (i+1) in
 	    findtype 1 in
 
-  let evalct = nf_ise1 env !isevars cj.uj_type
-  and evalPt = nf_ise1 env !isevars pj.uj_type in
+  let evalct = nf_ise1 !isevars cj.uj_type
+  and evalPt = nf_ise1 !isevars pj.uj_type in
 
   let (mind,bty,rsty) =
     Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
@@ -474,20 +476,20 @@ let j_apply f env sigma j =
 let ise_resolve fail_evar sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine mt_tycon false isevars metamap env c in
-  j_apply (process_evars fail_evar) env !isevars j
+  j_apply (fun _ -> process_evars fail_evar) env !isevars j
 
 
 let ise_resolve_type fail_evar sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine def_vty_con false isevars metamap env c in
   let tj = inh_ass_of_j env isevars j in
-  typed_app (strong (process_evars fail_evar) env !isevars) tj
+  typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj
 
 
 let ise_resolve_nocheck sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine mt_tycon true isevars metamap env c in
-  j_apply (process_evars true) env !isevars j
+  j_apply (fun _ -> process_evars true) env !isevars j
 
 
 let ise_resolve1 is_ass sigma env c =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b4fee1cd29..84097f8581 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -40,24 +40,25 @@ i*)
 
 (* Raw calls to the inference machine of Trad: boolean says if we must fail
  * on unresolved evars, or replace them by Metas *)
-val ise_resolve : bool -> 'c evar_map -> (int * constr) list ->
+val ise_resolve : bool -> unit evar_map -> (int * constr) list ->
   unsafe_env -> rawconstr -> unsafe_judgment
-val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list ->
+val ise_resolve_type : bool -> unit evar_map -> (int * constr) list ->
   unsafe_env -> rawconstr -> typed_type
 
 (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
  * if we must coerce to a type *)
-val ise_resolve1 : bool -> 'c evar_map -> unsafe_env -> rawconstr -> constr
+val ise_resolve1 : bool -> unit evar_map -> unsafe_env -> rawconstr -> constr
 
 (* progmach.ml tries to type ill-typed terms: does not perform the conversion
  * test in application.
  *)
-val ise_resolve_nocheck : 'c evar_map -> (int * constr) list ->
+val ise_resolve_nocheck : unit evar_map -> (int * constr) list ->
   unsafe_env -> rawconstr -> unsafe_judgment
 
 
 (* Internal of Trad...
  * Unused outside Trad, but useful for debugging
  *)
-val pretype : bool * (constr option * constr option) 
-  -> unsafe_env -> 'c evar_defs -> rawconstr -> unsafe_judgment
+val pretype : 
+  trad_constraint -> unsafe_env -> unit evar_defs -> rawconstr 
+    -> unsafe_judgment
diff --git a/proofs/typing_ev.ml b/pretyping/typing.ml
index 741ef10409..c12f9bb34f 100644
--- a/proofs/typing_ev.ml
+++ b/pretyping/typing.ml
@@ -149,6 +149,7 @@ let execute_type env sigma constr =
   let j = execute { fix=false; nocheck=true } env sigma constr in
   assumption_of_judgment env sigma j
 
-let execute_type env sigma constr = 
+let execute_rec_type env sigma constr = 
   let j = execute { fix=false; nocheck=false } env sigma constr in
   assumption_of_judgment env sigma j
+
diff --git a/proofs/typing_ev.mli b/pretyping/typing.mli
index b12cd369d3..b12cd369d3 100644
--- a/proofs/typing_ev.mli
+++ b/pretyping/typing.mli
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4c14040bdd..80aae11823 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,7 +33,7 @@ type 'a clausenv = {
 type wc = walking_constraints
 
 let new_evar_in_sign env =
-  let hyps = get_globals (Environ.context env) in
+  let hyps = Environ.var_context env in
   let ev = new_evar () in
   DOPN(Evar ev,
        Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
@@ -881,10 +881,10 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
-  failwith "TODO: clenv_type_of"
+  failwith "TODO"
   (***
-  (Trad.ise_resolve true (w_Underlying ce.hook) metamap
-     (gLOB(w_hyps ce.hook)) c)._TYPE
+  (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
+     (gLOB(w_hyps ce.hook)) c).uj_type
   ***)
 
 let clenv_instance_type_of ce c =
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index f3421cfdcc..e63648576d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -10,7 +10,7 @@ open Term
 open Environ
 open Evd
 open Reduction
-open Typing_ev
+open Typing
 open Proof_trees
 open Logic
 open Refiner
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b0823c1b2d..f89c6e9b4e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -10,7 +10,7 @@ open Term
 open Sign
 open Environ
 open Reduction
-open Typing_ev
+open Typing
 open Proof_trees
 open Typeops
 open Coqast
@@ -215,7 +215,7 @@ let move_after with_dep toleft (left,htfrom,right) hto =
 
 let prim_refiner r sigma goal =
   let env = goal.evar_env in
-  let sign = get_globals (context env) in
+  let sign = var_context env in
   let cl = goal.evar_concl in
   let info = goal.evar_info in
   match r with
@@ -401,8 +401,8 @@ let prim_refiner r sigma goal =
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
 let abst_value c =
-  let env = Global.env () in
-  Environ.abst_value (Typing.unsafe_env_of_env env) c
+  let env = Global.unsafe_env () in
+  Environ.abst_value env c
 	  
 let extract_constr = 
   let rec crec vl = function
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2b2f9b8b44..88b632882e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -15,8 +15,8 @@ open Proof_trees
 val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
 
 val prim_extractor : 
-  ((typed_type, constr) env -> proof_tree -> constr) -> 
-    (typed_type, constr) env -> proof_tree -> constr
+  ((typed_type, constr) sign -> proof_tree -> constr) -> 
+    (typed_type, constr) sign -> proof_tree -> constr
 
 val extract_constr : constr assumptions -> constr -> constr
 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 3523f42182..ee0f3de895 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,7 +8,7 @@ open Sign
 open Evd
 open Stamps
 open Environ
-open Typing_ev
+open Typing
 
 type bindOcc = 
   | Dep of identifier
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 834ee67343..1dc43f4134 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -714,7 +714,7 @@ let extract_pftreestate pts =
       [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
          'sPC; 'sTR"Please ascend to the root" >];
   let env = pts.tpf.goal.evar_env in
-  let hyps = get_globals (Environ.context env) in
+  let hyps = Environ.var_context env in
   strong whd_betadeltatiota env (ts_it pts.tpfsigma)
     (extract_proof hyps pts.tpf)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8bb6fba486..85f2973c03 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -11,7 +11,7 @@ open Instantiate
 open Environ
 open Reduction
 open Evd
-open Typing_ev
+open Typing
 open Tacred
 open Proof_trees
 open Logic
@@ -45,7 +45,7 @@ let pf_concl gls = (sig_it gls).evar_concl
 
 let pf_untyped_hyps gls  =
   let env = pf_env gls in
-  let (idl,tyl) = get_globals (Environ.context env) in 
+  let (idl,tyl) = Environ.var_context env in 
   (idl, List.map (fun x -> x.body) tyl)
 
 let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
@@ -69,6 +69,14 @@ let hnf_type_of gls =
 let pf_check_type gls c1 c2 =
   let casted = mkCast c1 c2 in pf_type_of gls casted
 
+let pf_constr_of_com gls c =
+  let evc = project gls in 
+  Astterm.constr_of_com evc (sig_it gls).hyps c
+
+let pf_constr_of_com_sort gls c =
+  let evc = project gls in 
+  Astterm.constr_of_com_sort evc (sig_it gls).hyps c
+
 let pf_reduction_of_redexp gls re c = 
   reduction_of_redexp re (pf_env gls) (project gls) c 
 
@@ -242,7 +250,7 @@ let mutual_cofix lf lar pf =
     
 let rename_bound_var_goal gls =
   let { evar_env = env; evar_concl = cl } as gl = sig_it gls in 
-  let ids = ids_of_sign (get_globals (Environ.context env)) in
+  let ids = ids_of_sign (Environ.var_context env) in
   convert_concl (rename_bound_var ids cl) gls
     
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 863023b79a..ea13c75a79 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,6 +41,9 @@ val pf_check_type         : goal sigma -> constr -> constr -> constr
 val pf_fexecute           : goal sigma -> constr -> unsafe_judgment
 val hnf_type_of           : goal sigma -> constr -> constr
 
+val pf_constr_of_com      : goal sigma -> Coqast.t -> constr
+val pf_constr_of_com_sort : goal sigma -> Coqast.t -> constr
+
 val pf_get_hyp             : goal sigma -> identifier -> constr
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 634e71f99a..2dc69c55bf 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,7 @@ open Sign
 open Inductive
 open Evd
 open Reduction
-open Typing_ev
+open Typing
 open Tacmach
 open Proof_trees
 open Pfedit
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 3fe9430c8c..2505f3b0a3 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -100,13 +100,13 @@ let dyn_decompose args gl =
   match args with 
     | [Clause ids; Command c] -> 
         decompose_these (pf_constr_of_com gl c) ids gl
-    | [CLAUSE ids; Constr c]  -> 
+    | [Clause ids; Constr c]  -> 
         decompose_these c ids  gl
     | l -> bad_tactic_args "DecomposeThese" l gl
 	  
 let h_decompose =
   let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in 
-  fun ids c -> v_decompose [(CLAUSE ids);(CONSTR c)] 
+  fun ids c -> v_decompose [Clause ids; Constr c] 
 
 let vernac_decompose_and = 
   hide_constr_tactic "DecomposeAnd" decompose_and
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 04f96a8721..419488a37b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -273,17 +273,17 @@ let explain_refiner_cannot_applt k ctx t harg =
        P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
        P.pr_term k ctx harg >]
 
-let error_occur_check ev rhs =
+let explain_occur_check k ctx ev rhs =
   let id = "?" ^ string_of_int ev in
-  let pt = prterm rhs in
+  let pt = P.pr_term k ctx rhs in
   errorlabstrm "Trad.occur_check"
     [< 'sTR"Occur check failed: tried to define "; 'sTR id;
       'sTR" with term"; 'bRK(1,1); pt >]
 
-let error_not_clean sp t =
-  let c = Rel (List.hd (Listset.elements(free_rels t))) in
+let explain_not_clean k ctx sp t =
+  let c = Rel (Intset.choose (free_rels t)) in
   let id = string_of_id (Names.basename sp) in
-  let var = pTERM(c) in
+  let var = P.pr_term k ctx c in
   errorlabstrm "Trad.not_clean"
     [< 'sTR"Tried to define "; 'sTR id;
        'sTR" with a term using variable "; var; 'sPC;
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 7a16930698..02620168c1 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -10,7 +10,7 @@ open Sign
 open Constant
 open Inductive
 open Type_errors
-open Typing
+open Safe_typing
 open G_minicoq
 
 let (env : environment ref) = ref empty_environment