MAJ pour fusion avec pretyping

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

21 files changed, 355 insertions, 117 deletions

diff --git a/.depend b/.depend
index cd9716d2cf..4e90f43227 100644
--- a/.depend
+++ b/.depend
@@ -48,7 +48,7 @@ library/nametab.cmi: kernel/names.cmi
 library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
-parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
+parsing/astterm.cmi: kernel/evd.cmi kernel/names.cmi pretyping/rawterm.cmi \
     kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
 parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
@@ -57,7 +57,24 @@ parsing/pcoq.cmi: parsing/coqast.cmi
 parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
-pretyping/astterm.cmi: kernel/evd.cmi kernel/names.cmi kernel/term.cmi 
+pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
+    library/libobject.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi 
+pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+    kernel/evd.cmi kernel/sign.cmi kernel/term.cmi 
+pretyping/evarconv.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi 
+pretyping/evarutil.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi 
+pretyping/pretype_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/type_errors.cmi 
+pretyping/pretyping.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
+pretyping/rawterm.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/type_errors.cmi 
+pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \
+    library/libobject.cmi library/library.cmi kernel/names.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 \
@@ -111,6 +128,8 @@ toplevel/mltop.cmi: library/libobject.cmi
 toplevel/protectedtoplevel.cmi: lib/pp.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
 toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
+toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
+    toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_trees.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
@@ -189,14 +208,16 @@ 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/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/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/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/evd.cmi \
     kernel/generic.cmi kernel/indtypes.cmi kernel/inductive.cmi \
     kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
@@ -305,6 +326,16 @@ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
     parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
+parsing/astterm.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \
+    kernel/evd.cmi kernel/generic.cmi toplevel/himsg.cmi kernel/names.cmi \
+    parsing/pcoq.cmi lib/pp.cmi parsing/printer.cmi pretyping/rawterm.cmi \
+    kernel/term.cmi parsing/termast.cmi toplevel/vernac.cmi \
+    parsing/astterm.cmi 
+parsing/astterm.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/environ.cmx \
+    kernel/evd.cmx kernel/generic.cmx toplevel/himsg.cmx kernel/names.cmx \
+    parsing/pcoq.cmi lib/pp.cmx parsing/printer.cmi pretyping/rawterm.cmi \
+    kernel/term.cmx parsing/termast.cmx toplevel/vernac.cmx \
+    parsing/astterm.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
@@ -315,16 +346,60 @@ parsing/termast.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
 parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/environ.cmx \
     kernel/generic.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
     lib/pp.cmx kernel/term.cmx lib/util.cmx parsing/termast.cmi 
-pretyping/astterm.cmo: parsing/ast.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/generic.cmi toplevel/himsg.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi parsing/printer.cmi kernel/term.cmi parsing/termast.cmi \
-    toplevel/vernac.cmi pretyping/astterm.cmi 
-pretyping/astterm.cmx: parsing/ast.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/generic.cmx toplevel/himsg.cmx kernel/names.cmx parsing/pcoq.cmi \
-    lib/pp.cmx parsing/printer.cmi kernel/term.cmx parsing/termast.cmx \
-    toplevel/vernac.cmx pretyping/astterm.cmi 
-pretyping/rawterm.cmo: kernel/names.cmi kernel/term.cmi 
-pretyping/rawterm.cmx: kernel/names.cmx kernel/term.cmx 
+pretyping/classops.cmo: kernel/environ.cmi kernel/generic.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/printer.cmi kernel/reduction.cmi kernel/term.cmi \
+    pretyping/classops.cmi 
+pretyping/classops.cmx: kernel/environ.cmx kernel/generic.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/printer.cmi kernel/reduction.cmx kernel/term.cmx \
+    pretyping/classops.cmi 
+pretyping/coercion.cmo: pretyping/classops.cmi pretyping/evarconv.cmi \
+    kernel/evd.cmi kernel/generic.cmi toplevel/himsg.cmi kernel/names.cmi \
+    pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi \
+    pretyping/coercion.cmi 
+pretyping/coercion.cmx: pretyping/classops.cmx pretyping/evarconv.cmx \
+    kernel/evd.cmx kernel/generic.cmx toplevel/himsg.cmx kernel/names.cmx \
+    pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx \
+    pretyping/coercion.cmi 
+pretyping/evarconv.cmo: pretyping/classops.cmi pretyping/evarutil.cmi \
+    kernel/generic.cmi kernel/names.cmi pretyping/recordops.cmi \
+    kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/evarconv.cmi 
+pretyping/evarconv.cmx: pretyping/classops.cmx pretyping/evarutil.cmx \
+    kernel/generic.cmx kernel/names.cmx pretyping/recordops.cmx \
+    kernel/reduction.cmx kernel/term.cmx lib/util.cmx pretyping/evarconv.cmi 
+pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    toplevel/himsg.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
+    kernel/reduction.cmi kernel/term.cmi pretyping/evarutil.cmi 
+pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    toplevel/himsg.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmi \
+    kernel/reduction.cmx kernel/term.cmx pretyping/evarutil.cmi 
+pretyping/pretype_errors.cmo: pretyping/pretype_errors.cmi 
+pretyping/pretype_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 \
+    library/indrec.cmi pretyping/multcase.cmi kernel/names.cmi lib/pp.cmi \
+    pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
+    pretyping/recordops.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
+    pretyping/pretyping.cmi 
+pretyping/pretyping.cmx: parsing/ast.cmx pretyping/classops.cmx \
+    pretyping/coercion.cmx kernel/environ.cmx pretyping/evarconv.cmx \
+    pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/indrec.cmx pretyping/multcase.cmi kernel/names.cmx lib/pp.cmx \
+    pretyping/pretype_errors.cmx pretyping/rawterm.cmi \
+    pretyping/recordops.cmx kernel/reduction.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
+    pretyping/pretyping.cmi 
+pretyping/recordops.cmo: pretyping/classops.cmi kernel/generic.cmi \
+    toplevel/himsg.cmi library/libobject.cmi library/library.cmi \
+    kernel/names.cmi lib/pp.cmi lib/pp_control.cmi kernel/term.cmi \
+    pretyping/recordops.cmi 
+pretyping/recordops.cmx: pretyping/classops.cmx kernel/generic.cmx \
+    toplevel/himsg.cmx library/libobject.cmx library/library.cmx \
+    kernel/names.cmx lib/pp.cmx lib/pp_control.cmx kernel/term.cmx \
+    pretyping/recordops.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 \
@@ -428,19 +503,19 @@ tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \
 tactics/btermdn.cmx: tactics/dn.cmx kernel/term.cmx tactics/termdn.cmx \
     tactics/btermdn.cmi 
 tactics/dhyp.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/generic.cmi \
-    toplevel/himsg.cmi library/lib.cmi library/libobject.cmi \
-    library/library.cmi kernel/names.cmi tactics/nbtermdn.cmi \
-    tactics/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    kernel/reduction.cmi library/summary.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi tactics/dhyp.cmi 
+    library/lib.cmi library/libobject.cmi library/library.cmi \
+    kernel/names.cmi tactics/nbtermdn.cmi tactics/pattern.cmi lib/pp.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi library/summary.cmi \
+    proofs/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi tactics/dhyp.cmi 
 tactics/dhyp.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/generic.cmx \
-    toplevel/himsg.cmx library/lib.cmx library/libobject.cmx \
-    library/library.cmx kernel/names.cmx tactics/nbtermdn.cmx \
-    tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    kernel/reduction.cmx library/summary.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx tactics/dhyp.cmi 
+    library/lib.cmx library/libobject.cmx library/library.cmx \
+    kernel/names.cmx tactics/nbtermdn.cmx tactics/pattern.cmx lib/pp.cmx \
+    proofs/proof_trees.cmx kernel/reduction.cmx library/summary.cmx \
+    proofs/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx tactics/dhyp.cmi 
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
 tactics/elim.cmo: proofs/clenv.cmi kernel/generic.cmi tactics/hiddentac.cmi \
@@ -519,12 +594,12 @@ toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
     toplevel/errors.cmi 
-toplevel/himsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi 
-toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
-    lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
+toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi kernel/generic.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi 
+toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx kernel/generic.cmx \
+    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
+    kernel/term.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 \
@@ -533,12 +608,12 @@ 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 
-toplevel/mltop.cmo: library/libobject.cmi library/library.cmi lib/pp.cmi \
-    library/summary.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/mltop.cmi 
-toplevel/mltop.cmx: library/libobject.cmx library/library.cmx lib/pp.cmx \
-    library/summary.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/mltop.cmi 
+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 
+toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
+    lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx toplevel/mltop.cmi 
 toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
     lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \
     toplevel/protectedtoplevel.cmi 
@@ -561,11 +636,29 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     toplevel/vernac.cmi 
+toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \
+    pretyping/classops.cmi parsing/coqast.cmi library/declare.cmi \
+    kernel/environ.cmi kernel/evd.cmi library/libobject.cmi \
+    library/library.cmi proofs/macros.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi lib/pp_control.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 
+toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \
+    pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \
+    kernel/environ.cmx kernel/evd.cmx library/libobject.cmx \
+    library/library.cmx proofs/macros.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmx lib/pp_control.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 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
-    toplevel/errors.cmi toplevel/himsg.cmi kernel/names.cmi lib/pp.cmi \
+    toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \
-    toplevel/errors.cmx toplevel/himsg.cmx kernel/names.cmx lib/pp.cmx \
+    toplevel/himsg.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     proofs/proof_trees.cmx proofs/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmi 
diff --git a/Makefile b/Makefile
index b4d60a98b3..9819598d03 100644
--- a/Makefile
+++ b/Makefile
@@ -11,7 +11,7 @@ noargument:
 	@echo or make archclean
 
 LOCALINCLUDES=-I config -I lib -I kernel -I library \
-              -I proofs -I tactics -I parsing -I toplevel
+              -I proofs -I tactics -I pretyping -I parsing -I toplevel
 INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
 BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
@@ -113,9 +113,10 @@ LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
 LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
 LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli)
 LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli)
+LPPRETYPING = pretyping/rawterm.mli $(PRETYPING:.cmo=.mli)
 LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli)
 LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \
-	  $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL)
+	  $(LPPROOFS) $(LPTACTICS) $(LPPRETYPING) $(LPTOPLEVEL)
 
 doc/coq.tex: doc/preamble.tex $(LPFILES)
 	cat doc/preamble.tex > doc/coq.tex
@@ -240,4 +241,4 @@ dependcamlp4: beforedepend
 	done
 
 include .depend
-include .depend.camlp4
\ No newline at end of file
+include .depend.camlp4
diff --git a/kernel/evd.ml b/kernel/evd.ml
index b31f2f6b79..b12e6e9930 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -20,7 +20,7 @@ type evar_body =
   | Evar_defined of constr
 
 type 'a evar_info = {
-  evar_concl : constr;
+  evar_concl : typed_type;
   evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 62378f921e..036443f129 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -23,7 +23,7 @@ type evar_body =
   | Evar_defined of constr
 
 type 'a evar_info = {
-  evar_concl : constr;
+  evar_concl : typed_type;
   evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 819dfcf841..37ffa5ca12 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -82,7 +82,8 @@ let existential_type sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
-  instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+  instantiate_constr (ids_of_sign hyps) (body_of_type info.evar_concl)
+    (Array.to_list args)
 
 let existential_value sigma c =
   let (n,args) = destEvar c in
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 9c2ffedb2f..26dc2b6170 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -234,4 +234,5 @@ let lookup_id id env =
 
 type 'b assumptions = (typed_type,'b) env
 type context = (typed_type,typed_type) env
+type var_context = typed_type signature
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index c67ab11d8f..af8dbe086f 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -83,4 +83,5 @@ val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
 
 type 'b assumptions = (typed_type,'b) env
 type context = (typed_type,typed_type) env
+type var_context = typed_type signature
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index db992769dd..eaef2dafc0 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -28,6 +28,7 @@ type type_error =
       * typed_type array
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
+  | CantFindCaseType of constr
 
 exception TypeError of path_kind * context * type_error
 
@@ -41,7 +42,7 @@ let error_not_type k env c =
   raise (TypeError (k, context env, NotAType c))
 
 let error_assumption k env c =
-    raise (TypeError (k, context env, BadAssumption c))
+  raise (TypeError (k, context env, BadAssumption c))
 
 let error_reference_variables k env id =
   raise (TypeError (k, context env, ReferenceVariables id))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index fae63666c1..23fed99f3e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -30,6 +30,7 @@ type type_error =
       * typed_type array
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
+  | CantFindCaseType of constr
 
 exception TypeError of path_kind * context * type_error
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 65406f2798..f20c5d213a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -175,6 +175,15 @@ let type_inst_construct env sigma i mind =
   with Induc -> 
     error_not_inductive CCI env 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 id = id_of_string ("?" ^ string_of_int ev) in
+  check_hyps id env sigma hyps;
+  instantiate_type (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
+
+
 (* Case. *)
 
 let rec sort_of_arity env sigma c =
@@ -338,14 +347,23 @@ let type_of_case env sigma pj cj lfj =
 
 (* Prop and Set *)
 
-let type_of_prop_or_set cts =
-  { uj_val = DOP0(Sort(Prop cts));
+let judge_of_prop =
+  { uj_val = DOP0(Sort prop);
+    uj_type = DOP0(Sort type_0);
+    uj_kind = DOP0(Sort type_1) }
+
+let judge_of_set =
+  { uj_val = DOP0(Sort spec);
     uj_type = DOP0(Sort type_0);
     uj_kind = DOP0(Sort type_1) }
 
+let make_judge_of_prop_contents = function
+  | Null -> judge_of_prop
+  | Pos -> judge_of_set
+
 (* Type of Type(i). *)
 
-let type_of_type u =
+let make_judge_of_type u =
   let (uu,uuu,c) = super_super u in
   { uj_val = DOP0 (Sort (Type u));
     uj_type = DOP0 (Sort (Type uu));
@@ -447,7 +465,7 @@ let apply_rel_list env sigma nocheck argjl funj =
  which may contain the CoFix variables. These occurrences of CoFix variables
  are not considered *)
 
-let noccur_with_meta lc n m term = 
+let noccur_with_meta n m term = 
   let rec occur_rec n = function
     | Rel p -> if n<=p & p<n+m then raise Occur
     | VAR _ -> ()
@@ -455,7 +473,7 @@ let noccur_with_meta lc n m term =
 	(match strip_outer_cast cl.(0) with
            | DOP0 (Meta _) -> ()
 	   | _ -> Array.iter (occur_rec n) cl)
-    | DOPN(Const sp, cl) when Spset.mem sp lc -> ()
+    | DOPN(Evar _, _) -> ()
     | DOPN(op,cl) -> Array.iter (occur_rec n) cl
     | DOPL(_,cl) -> List.iter (occur_rec n) cl
     | DOP0(_) -> ()
@@ -587,7 +605,7 @@ let is_subterm env sigma lcx mind_recvec n lst c =
 (* Auxiliary function: it checks a condition f depending on a deBrujin
    index for a certain number of abstractions *)
 
-let rec check_subterm_rec_meta env sigma lc vectn k def = 
+let rec check_subterm_rec_meta env sigma vectn k def = 
   (k < 0) or
   (let nfi = Array.length vectn in 
    (* check fi does not appear in the k+1 first abstractions, 
@@ -595,7 +613,7 @@ let rec check_subterm_rec_meta env sigma lc vectn k def =
    let rec check_occur n def = 
      (match strip_outer_cast def with
 	| DOP2(Lambda,a,DLAM(_,b)) -> 
-	    if noccur_with_meta lc n nfi a then
+	    if noccur_with_meta n nfi a then
               if n = k+1 then (a,b) else check_occur (n+1) b
             else 
 	      error "Bad occurrence of recursive call"
@@ -613,7 +631,7 @@ let rec check_subterm_rec_meta env sigma lc vectn k def =
    *)
    let rec check_rec_call n lst t = 
      (* n gives the index of the recursive variable *)
-     (noccur_with_meta lc (n+k+1) nfi t) or 
+     (noccur_with_meta (n+k+1) nfi t) or 
      (* no recursive call in the term *)
      (match whd_betadeltaiota_stack env sigma t [] with 
 	| (Rel p,l) -> 
@@ -726,7 +744,7 @@ nvect is [|n1;..;nk|] which gives for each recursive definition
 the inductive-decreasing index 
 the function checks the convertibility of ti with Ai *)
 
-let check_fix env sigma lc = function
+let check_fix env sigma = function
   | DOPN(Fix(nvect,j),vargs) -> 
       let nbfix = let nv = Array.length vargs in 
       if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
@@ -742,7 +760,7 @@ let check_fix env sigma lc = function
 	let check_type i = 
 	  try
 	    let _ = 
-	      check_subterm_rec_meta env sigma lc nvect nvect.(i) vdefs.(i) in 
+	      check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in 
 	    ()
 	  with UserError (s,str) ->
 	    error_ill_formed_rec_body CCI env str lna i vdefs 
@@ -756,7 +774,7 @@ let check_fix env sigma lc = function
 let mind_nparams env i =
   let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
 
-let check_guard_rec_meta env sigma lc nbfix def deftype = 
+let check_guard_rec_meta env sigma nbfix def deftype = 
   let rec codomain_is_coind c  =
     match whd_betadeltaiota env sigma (strip_outer_cast c) with
       | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b 
@@ -771,7 +789,7 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
   let lvlra = (mis_recargs (lookup_mind_specif mI env)) in
   let vlra = lvlra.(tyi) in  
   let rec check_rec_call alreadygrd n vlra  t = 
-    if noccur_with_meta lc n nbfix t then
+    if noccur_with_meta n nbfix t then
       true 
     else 
       match whd_betadeltaiota_stack env sigma t [] with 
@@ -781,7 +799,7 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
              if n <= p && p < n+nbfix then
 	       (* recursive call *)
                if alreadygrd then
-		 if List.for_all (noccur_with_meta lc n nbfix) l then
+		 if List.for_all (noccur_with_meta n nbfix) l then
 		   true
 		 else 
 		   error "Nested recursive occurrences"
@@ -820,19 +838,21 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
                                (process_args_of_constr lr lrar)
 				 
                        |  _::lrar  -> 
-                            if (noccur_with_meta lc n nbfix t) 
+                            if (noccur_with_meta n nbfix t) 
                             then (process_args_of_constr lr lrar)
                             else error "Recursive call inside a non-recursive argument of constructor")
             in (process_args_of_constr realargs lra)
 		 
 		 
 	| (DOP2(Lambda,a,DLAM(_,b)),[]) -> 
-            if (noccur_with_meta lc n nbfix a) then
+            if (noccur_with_meta n nbfix a) then
               check_rec_call alreadygrd (n+1)  vlra b
             else 
 	      error "Recursive call in the type of an abstraction"
 	      
 	| (DOPN(CoFix(j),vargs),l) -> 
+          if  (List.for_all (noccur_with_meta n nbfix) l)
+          then 
             let nbfix = let nv = Array.length vargs in 
             if nv < 2 then
               error "Ill-formed recursive definition" 
@@ -845,18 +865,19 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
             let (lna,vdefs) = decomp_DLAMV_name la ldef in
             let vlna = Array.of_list lna 
             in 
-	    if (array_for_all (noccur_with_meta lc n nbfix) varit) then
+	    if (array_for_all (noccur_with_meta n nbfix) varit) then
               (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
               &&
               (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) 
             else 
 	      error "Recursive call in the type of a declaration"
-		
+	  else error "Unguarded recursive call"
+
 	| (DOPN(MutCase _,_) as mc,l) -> 
             let (_,p,c,vrest) = destCase mc in
-            if (noccur_with_meta lc n nbfix p) then
-              if (noccur_with_meta lc n nbfix c) then
-		if (List.for_all (noccur_with_meta lc n nbfix) l) then
+            if (noccur_with_meta n nbfix p) then
+              if (noccur_with_meta n nbfix c) then
+		if (List.for_all (noccur_with_meta n nbfix) l) then
 		  (array_for_all (check_rec_call alreadygrd n vlra) vrest)
 		else 
 		  error "Recursive call in the argument of a function defined by cases"        
@@ -873,7 +894,7 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
 (* The  function which checks that the whole block of definitions 
    satisfies the guarded condition *)
 
-let check_cofix env sigma lc f = 
+let check_cofix env sigma f = 
   match f with
     | DOPN(CoFix(j),vargs) -> 
 	let nbfix = let nv = Array.length vargs in 
@@ -890,7 +911,7 @@ let check_cofix env sigma lc f =
 	let check_type i = 
 	  try 
 	    let _ = 
-	      check_guard_rec_meta env sigma lc nbfix vdefs.(i) varit.(i) in 
+	      check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in 
 	    ()
 	  with UserError (s,str) -> 
 	    error_ill_formed_rec_body CCI env str lna i vdefs 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 45db129741..1e602e0397 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -32,6 +32,8 @@ val type_of_inductive : unsafe_env -> 'a evar_map -> constr -> typed_type
 
 val type_of_constructor : unsafe_env -> 'a evar_map -> constr -> constr
 
+val type_of_existential : unsafe_env -> 'a evar_map -> constr -> typed_type
+
 val type_of_case : unsafe_env -> 'a evar_map 
   -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment array -> unsafe_judgment
@@ -40,9 +42,9 @@ val type_case_branches :
   unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
     -> constr * constr array * constr 
 
-val type_of_prop_or_set : contents -> unsafe_judgment
+val make_judge_of_prop_contents : contents -> unsafe_judgment
 
-val type_of_type : universe -> unsafe_judgment * constraints
+val make_judge_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
   unsafe_env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
@@ -60,8 +62,8 @@ val apply_rel_list :
   unsafe_env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
     -> unsafe_judgment * constraints
 
-val check_fix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
-val check_cofix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
+val check_fix : unsafe_env -> 'a evar_map -> constr -> unit
+val check_cofix : unsafe_env -> 'a evar_map -> constr -> unit
 
 val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 27b50dceba..db3d00302e 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -79,20 +79,20 @@ let rec execute mf env cstr =
           error "General Fixpoints not allowed";
         let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
-        check_fix env Evd.empty Spset.empty fix;
+        check_fix env Evd.empty fix;
 	(make_judge fix larv.(i), cst)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
         let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
-        check_cofix env Evd.empty Spset.empty cofix;
+        check_cofix env Evd.empty cofix;
 	(make_judge cofix larv.(i), cst)
 	  
     | IsSort (Prop c) -> 
-	(type_of_prop_or_set c, cst0)
+	(make_judge_of_prop_contents c, cst0)
 
     | IsSort (Type u) ->
-	type_of_type u
+	make_judge_of_type u
 	  
     | IsAppL (f,args) ->
 	let (j,cst1) = execute mf env f in
diff --git a/lib/util.mli b/lib/util.mli
index 506b63cbda..e0462b36c9 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -53,7 +53,6 @@ val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
-val list_distinct : 'a list -> bool
 val list_subset : 'a list -> 'a list -> bool
 val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_firstn : int -> 'a list -> 'a list
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 0f3113bf60..c6fee417b0 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -1,24 +1,44 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                               astterm.mli                                *)
+(****************************************************************************)
 
-(* $Id$ *)
-
-(*i*)
 open Names
 open Term
-open Environ
-(*i*)
+open Evd
+open Rawterm
+
+(*
+val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
+val dbize    : unit assumptions -> CoqAst.t -> constr
 
-val dbize_op : 
-  Coqast.loc -> string -> Coqast.t list -> pseudo_constr list -> pseudo_constr
-val dbize    : unit assumptions -> Coqast.t -> pseudo_constr
+val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
+*)
+val dbize_cci      : 'c evar_map -> unit assumptions -> CoqAst.t -> rawconstr
 
-val absolutize_cci : unsafe_env -> pseudo_constr -> pseudo_constr
-val dbize_cci      : unsafe_env -> Coqast.t -> pseudo_constr
-val absolutize_fw  : unsafe_env -> pseudo_constr -> pseudo_constr
-val dbize_fw       : unsafe_env -> Coqast.t -> pseudo_constr
+(*
+val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
+*)
+val dbize_fw       : 'c evar_map -> unit assumptions -> CoqAst.t -> rawconstr
 
-val raw_pseudo_constr_of_com : unsafe_env -> Coqast.t -> pseudo_constr
-val raw_fpseudo_constr_of_com : unsafe_env -> Coqast.t -> pseudo_constr
-val raw_pseudo_constr_of_compattern : unsafe_env -> Coqast.t -> pseudo_constr
+val raw_constr_of_com :
+  'c evar_map -> 'a assumptions -> CoqAst.t -> rawconstr
+val raw_fconstr_of_com :
+  'c evar_map -> 'a assumptions -> CoqAst.t -> rawconstr
+val raw_constr_of_compattern :
+  'c evar_map -> 'a assumptions -> CoqAst.t -> rawconstr
 
-val globalize_command : Coqast.t -> Coqast.t
-val globalize_ast     : Coqast.t -> Coqast.t
+val globalize_command : CoqAst.t -> CoqAst.t
+val globalize_ast     : CoqAst.t -> CoqAst.t
+
+(* $Id$ *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index cab7a15d2f..7b95e2dcc6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,2 +1,80 @@
 
 (* $Id$ *)
+
+(*i*)
+open Names
+open Sign
+open Term
+open Environ
+open Evd
+open Rawterm
+(*i*)
+
+val type_of_com : context -> Coqast.t -> typed_type
+
+val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr ->
+  constr
+
+val constr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com : 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+
+val fconstr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com : 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+
+
+(* Typing with Trad, and re-checking with Mach *)
+(*i
+val fconstruct :'c evar_map -> context -> Coqast.t -> judgement
+val fconstruct_type :
+  'c evar_map -> context -> Coqast.t -> type_judgement
+
+val infconstruct_type :
+  'c evar_map -> (context * context) ->
+    Coqast.t -> type_judgement * information
+val infconstruct :
+  'c evar_map -> (context * context) ->
+    Coqast.t -> judgement * information
+
+(* Typing, re-checking with universes constraints *)
+val fconstruct_with_univ :
+  'c evar_map -> context -> Coqast.t -> judgement
+val fconstruct_with_univ_sp : 'c evar_map -> context
+  -> section_path -> constr -> Impuniv.universes * judgement
+val fconstruct_type_with_univ_sp : 'c evar_map -> context
+  -> section_path -> constr -> Impuniv.universes * type_judgement
+val infconstruct_with_univ_sp :
+  'c evar_map -> (context * context)
+  -> section_path -> constr -> Impuniv.universes * (judgement * information)
+val infconstruct_type_with_univ_sp :
+  'c evar_map -> (context * context)
+  -> section_path -> constr 
+  -> Impuniv.universes * (type_judgement * information)
+i*)
+
+(* Low level typing functions, for terms with de Bruijn indices and Metas *)
+
+(* 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 ->
+  context -> rawconstr -> unsafe_judgment
+val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list ->
+  context -> 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 -> context -> 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 ->
+  context -> rawconstr -> unsafe_judgment
+
+
+(* Internal of Trad...
+ * Unused outside Trad, but useful for debugging
+ *)
+val pretype : bool * (constr option * constr option) -> 'c evar_map ref
+  -> context -> rawconstr -> unsafe_judgment
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d30de0647b..0ee1e04349 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -1,5 +1,15 @@
+
+(* $Id$ *)
+
+(*i*)
 open Names
-open CoqAst
+open Sign
+open Type_errors
+(*i*)
+
+(* Untyped intermediate terms, after ASTs and before constr. *)
+
+type loc = int * int
 
 type indtype_id = section_path * int
 type constructor_id = indtype_id * int
@@ -39,7 +49,8 @@ type rawconstr =
   | RHole of loc option
   | RCast of loc * rawconstr * rawconstr
 
-(* - if PRec (_, names, arities, bodies) is in env then arities are
+
+(*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
    arities incrementally lifted 
 
@@ -48,4 +59,4 @@ type rawconstr =
 
    - boolean in POldCase means it is recursive
    - option in PHole tell if the "?" was apparent or has been implicitely added
-*)
+i*)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b0823c1b2d..11f978d4dc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -221,7 +221,7 @@ let prim_refiner r sigma goal =
   match r with
     | { name = Intro; newids = [id] } ->
     	if mem_sign sign id then error "New variable is already declared";
-        (match strip_outer_cast cl with
+        (match strip_outer_cast cl.body with
 	   | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = mk_assumption env sigma c1
@@ -232,7 +232,7 @@ let prim_refiner r sigma goal =
 	
     | { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
     	if mem_sign sign id then error "New variable is already declared";
-        (match strip_outer_cast cl with
+        (match strip_outer_cast cl.body with
 	   | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       if not (List.for_all
@@ -248,7 +248,7 @@ let prim_refiner r sigma goal =
 	   | _ -> error "Introduction needs a product")
 	
     | { name = Intro_replacing; newids = []; hypspecs = [id] } ->
-	(match strip_outer_cast cl with
+	(match strip_outer_cast cl.body with
            | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       if not (List.for_all 
@@ -280,10 +280,10 @@ let prim_refiner r sigma goal =
 		  check_ind (k-1) b
             | _ -> error "not enough products"
 	in
-     	let _ = check_ind n cl in 
+     	let _ = check_ind n cl.body in 
 	if mem_sign sign f then error "name already used in the environment";
-        let a = mk_assumption env sigma cl in
-        let sg = mk_goal info (push_var (f,a) env) cl in
+        let a = mk_assumption env sigma cl.body in
+        let sg = mk_goal info (push_var (f,a) env) cl.body in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index d12dad6e25..a119354a01 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,6 +8,7 @@ open Sign
 open Evd
 open Stamps
 open Environ
+open Typing_ev
 
 type bindOcc = 
   | Dep of identifier
@@ -95,7 +96,8 @@ let lc_toList lc = Intset.elements lc
 (* Functions on goals *)
 
 let mk_goal ctxt env cl = 
-  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
+  let ty = execute_type env Evd.empty cl in
+  { evar_env = env; evar_concl = ty; evar_body = Evar_empty; evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
index 6bf2dd9119..54a9d42dce 100644
--- a/proofs/typing_ev.ml
+++ b/proofs/typing_ev.ml
@@ -60,20 +60,20 @@ let rec execute mf env sigma cstr =
           error "General Fixpoints not allowed";
         let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
-        check_fix env sigma Spset.empty fix;
+        check_fix env sigma fix;
 	make_judge fix larv.(i)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
         let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
-        check_cofix env sigma Spset.empty cofix;
+        check_cofix env sigma cofix;
 	make_judge cofix larv.(i)
 	  
     | IsSort (Prop c) -> 
-	type_of_prop_or_set c
+	make_judge_of_prop_contents c
 
     | IsSort (Type u) ->
-	let (j,_) = type_of_type u in j
+	let (j,_) = make_judge_of_type u in j
 	  
     | IsAppL (f,args) ->
 	let j = execute mf env sigma f in
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index bdc0faf27c..e4d79051c9 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -110,7 +110,6 @@ open Names
 open Generic
 open Term
 open Reduction
-open Himsg
 open Proof_trees
 open Tacmach
 open Tactics
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 07c35ab321..53b35ff6d1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -212,7 +212,14 @@ let explain_ml_case k ctx mes c ct br brt =
   hOV 0 [< 'sTR "In ML case expression on "; pc; 'wS 1; 'cUT ;
            'sTR "of type";  'wS 1; pct; 'wS 1; 'cUT; 
            'sTR "which is an inductive predicate."; 'fNL; expln >]
-
+(*
+let explain_cant_find_case_type loc k ctx c =
+  let pe = P.pr_term k ctx c in
+  Ast.user_err_loc
+    (loc,"pretype",
+     hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
+	     'wS 1; pe >])
+*)
 let explain_type_error k ctx = function
   | UnboundRel n -> 
       explain_unbound_rel k ctx n