maj

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

2 files changed, 75 insertions, 62 deletions

diff --git a/.depend b/.depend
index aeecfba5e5..263b4652be 100644
--- a/.depend
+++ b/.depend
@@ -465,11 +465,6 @@ contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi
 contrib/rtauto/refl_tauto.cmi: kernel/term.cmi proofs/tacmach.cmi \
     proofs/proof_type.cmi contrib/rtauto/proof_search.cmi kernel/names.cmi 
 contrib/subtac/eterm.cmi: proofs/tacmach.cmi pretyping/evd.cmi 
-contrib/subtac/infer.cmi: lib/util.cmi kernel/term.cmi \
-    contrib/subtac/sast.cmo lib/pp.cmi contrib/subtac/natural.cmo \
-    kernel/names.cmi 
-contrib/subtac/rewrite.cmi: kernel/term.cmi contrib/subtac/scoq.cmo \
-    contrib/subtac/sast.cmo kernel/names.cmi 
 contrib/xml/doubleTypeInference.cmi: kernel/term.cmi kernel/names.cmi \
     pretyping/evd.cmi kernel/environ.cmi contrib/xml/acic.cmo 
 contrib/xml/xmlcommand.cmi: contrib/xml/xml.cmi kernel/term.cmi \
@@ -3402,18 +3397,20 @@ contrib/setoid_ring/newring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     pretyping/evd.cmx kernel/esubst.cmx kernel/environ.cmx \
     parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \
     kernel/closure.cmx toplevel/cerrors.cmx 
+contrib/subtac/context.cmo: kernel/term.cmi kernel/names.cmi \
+    kernel/environ.cmi 
+contrib/subtac/context.cmx: kernel/term.cmx kernel/names.cmx \
+    kernel/environ.cmx 
 contrib/subtac/eterm.cmo: pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
-    contrib/subtac/sutils.cmi kernel/reduction.cmi lib/pp.cmi \
-    kernel/names.cmi library/global.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi kernel/environ.cmi library/declare.cmi \
-    library/decl_kinds.cmo contrib/subtac/eterm.cmi 
+    kernel/reduction.cmi lib/pp.cmi kernel/names.cmi library/global.cmi \
+    pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
+    library/declare.cmi library/decl_kinds.cmo contrib/subtac/eterm.cmi 
 contrib/subtac/eterm.cmx: pretyping/termops.cmx kernel/term.cmx \
     tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \
-    contrib/subtac/sutils.cmx kernel/reduction.cmx lib/pp.cmx \
-    kernel/names.cmx library/global.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx kernel/environ.cmx library/declare.cmx \
-    library/decl_kinds.cmx contrib/subtac/eterm.cmi 
+    kernel/reduction.cmx lib/pp.cmx kernel/names.cmx library/global.cmx \
+    pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \
+    library/declare.cmx library/decl_kinds.cmx contrib/subtac/eterm.cmi 
 contrib/subtac/g_eterm.cmo: lib/util.cmi proofs/tacmach.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
     parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi contrib/subtac/eterm.cmi \
@@ -3422,62 +3419,78 @@ contrib/subtac/g_eterm.cmx: lib/util.cmx proofs/tacmach.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \
     parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx contrib/subtac/eterm.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
-contrib/subtac/infer.cmo: lib/util.cmi toplevel/toplevel.cmi kernel/term.cmi \
-    contrib/subtac/scoq.cmo contrib/subtac/sast.cmo pretyping/rawterm.cmi \
-    parsing/printer.cmi lib/pp.cmi contrib/subtac/natural.cmo \
-    library/nametab.cmi kernel/names.cmi library/libnames.cmi \
-    pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \
-    kernel/declarations.cmi contrib/subtac/infer.cmi 
-contrib/subtac/infer.cmx: lib/util.cmx toplevel/toplevel.cmx kernel/term.cmx \
-    contrib/subtac/scoq.cmx contrib/subtac/sast.cmx pretyping/rawterm.cmx \
-    parsing/printer.cmx lib/pp.cmx contrib/subtac/natural.cmx \
-    library/nametab.cmx kernel/names.cmx library/libnames.cmx \
-    pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \
-    kernel/declarations.cmx contrib/subtac/infer.cmi 
-contrib/subtac/rewrite.cmo: lib/util.cmi kernel/univ.cmi pretyping/typing.cmi \
-    pretyping/termops.cmi kernel/term.cmi kernel/sign.cmi \
-    contrib/subtac/scoq.cmo kernel/reduction.cmi parsing/printer.cmi \
-    lib/pp.cmi proofs/pfedit.cmi contrib/subtac/natural.cmo kernel/names.cmi \
-    library/libnames.cmi contrib/subtac/infer.cmi pretyping/inductiveops.cmi \
-    kernel/inductive.cmi library/global.cmi pretyping/evd.cmi \
-    contrib/subtac/eterm.cmi kernel/environ.cmi kernel/declarations.cmi \
-    library/decl_kinds.cmo interp/coqlib.cmi toplevel/command.cmi \
-    contrib/subtac/rewrite.cmi 
-contrib/subtac/rewrite.cmx: lib/util.cmx kernel/univ.cmx pretyping/typing.cmx \
-    pretyping/termops.cmx kernel/term.cmx kernel/sign.cmx \
-    contrib/subtac/scoq.cmx kernel/reduction.cmx parsing/printer.cmx \
-    lib/pp.cmx proofs/pfedit.cmx contrib/subtac/natural.cmx kernel/names.cmx \
-    library/libnames.cmx contrib/subtac/infer.cmx pretyping/inductiveops.cmx \
-    kernel/inductive.cmx library/global.cmx pretyping/evd.cmx \
-    contrib/subtac/eterm.cmx kernel/environ.cmx kernel/declarations.cmx \
-    library/decl_kinds.cmx interp/coqlib.cmx toplevel/command.cmx \
-    contrib/subtac/rewrite.cmi 
-contrib/subtac/sast.cmo: lib/util.cmi kernel/names.cmi 
-contrib/subtac/sast.cmx: lib/util.cmx kernel/names.cmx 
-contrib/subtac/scoq.cmo: kernel/term.cmi lib/pp.cmi \
-    contrib/subtac/natural.cmo kernel/names.cmi library/libnames.cmi \
-    library/global.cmi pretyping/evd.cmi interp/coqlib.cmi \
-    interp/constrintern.cmi interp/constrextern.cmi 
-contrib/subtac/scoq.cmx: kernel/term.cmx lib/pp.cmx \
-    contrib/subtac/natural.cmx kernel/names.cmx library/libnames.cmx \
-    library/global.cmx pretyping/evd.cmx interp/coqlib.cmx \
-    interp/constrintern.cmx interp/constrextern.cmx 
+contrib/subtac/interp.cmo: lib/util.cmi kernel/typeops.cmi \
+    kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
+    contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \
+    kernel/sign.cmi contrib/subtac/scoq.cmo pretyping/retyping.cmi \
+    pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \
+    parsing/printer.cmi pretyping/pretyping.cmi pretyping/pretype_errors.cmi \
+    lib/pp.cmi proofs/pfedit.cmi pretyping/pattern.cmi kernel/names.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+    lib/gset.cmi library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
+    lib/dyn.cmi kernel/declarations.cmi library/decl_kinds.cmo \
+    interp/coqlib.cmi contrib/subtac/context.cmo interp/constrintern.cmi \
+    toplevel/command.cmi pretyping/coercion.cmi pretyping/classops.cmi \
+    pretyping/cases.cmi 
+contrib/subtac/interp.cmx: lib/util.cmx kernel/typeops.cmx \
+    kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
+    contrib/subtac/subtac_errors.cmx contrib/subtac/subtac_coercion.cmx \
+    kernel/sign.cmx contrib/subtac/scoq.cmx pretyping/retyping.cmx \
+    pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \
+    parsing/printer.cmx pretyping/pretyping.cmx pretyping/pretype_errors.cmx \
+    lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx kernel/names.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+    lib/gset.cmx library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
+    lib/dyn.cmx kernel/declarations.cmx library/decl_kinds.cmx \
+    interp/coqlib.cmx contrib/subtac/context.cmx interp/constrintern.cmx \
+    toplevel/command.cmx pretyping/coercion.cmx pretyping/classops.cmx \
+    pretyping/cases.cmx 
+contrib/subtac/scoq.cmo: interp/topconstr.cmi pretyping/termops.cmi \
+    kernel/term.cmi kernel/sign.cmi parsing/printer.cmi \
+    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
+    library/libnames.cmi lib/gset.cmi library/global.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi kernel/environ.cmi interp/coqlib.cmi \
+    interp/constrextern.cmi 
+contrib/subtac/scoq.cmx: interp/topconstr.cmx pretyping/termops.cmx \
+    kernel/term.cmx kernel/sign.cmx parsing/printer.cmx \
+    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
+    library/libnames.cmx lib/gset.cmx library/global.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx kernel/environ.cmx interp/coqlib.cmx \
+    interp/constrextern.cmx 
 contrib/subtac/sparser.cmo: toplevel/vernacinterp.cmi \
     toplevel/vernacentries.cmi lib/util.cmi interp/topconstr.cmi \
     kernel/term.cmi proofs/tacexpr.cmo contrib/subtac/scoq.cmo \
-    contrib/subtac/sast.cmo contrib/subtac/rewrite.cmi kernel/reduction.cmi \
-    lib/pp.cmi parsing/pcoq.cmi lib/options.cmi kernel/names.cmi \
-    library/nameops.cmi library/libnames.cmi interp/genarg.cmi \
+    kernel/reduction.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \
+    kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+    contrib/subtac/interp.cmo interp/genarg.cmi kernel/environ.cmi \
     parsing/egrammar.cmi toplevel/cerrors.cmi 
 contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \
     toplevel/vernacentries.cmx lib/util.cmx interp/topconstr.cmx \
     kernel/term.cmx proofs/tacexpr.cmx contrib/subtac/scoq.cmx \
-    contrib/subtac/sast.cmx contrib/subtac/rewrite.cmx kernel/reduction.cmx \
-    lib/pp.cmx parsing/pcoq.cmx lib/options.cmx kernel/names.cmx \
-    library/nameops.cmx library/libnames.cmx interp/genarg.cmx \
+    kernel/reduction.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \
+    kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+    contrib/subtac/interp.cmx interp/genarg.cmx kernel/environ.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
-contrib/subtac/sutils.cmo: contrib/subtac/sutils.cmi 
-contrib/subtac/sutils.cmx: contrib/subtac/sutils.cmi 
+contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
+    kernel/term.cmi contrib/subtac/subtac_errors.cmo contrib/subtac/scoq.cmo \
+    pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
+    pretyping/recordops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
+    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
+    interp/coqlib.cmi contrib/subtac/context.cmo pretyping/classops.cmi 
+contrib/subtac/subtac_coercion.cmx: lib/util.cmx kernel/typeops.cmx \
+    kernel/term.cmx contrib/subtac/subtac_errors.cmx contrib/subtac/scoq.cmx \
+    pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
+    pretyping/recordops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
+    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
+    interp/coqlib.cmx contrib/subtac/context.cmx pretyping/classops.cmx 
+contrib/subtac/subtac_errors.cmo: lib/util.cmi parsing/printer.cmi lib/pp.cmi 
+contrib/subtac/subtac_errors.cmx: lib/util.cmx parsing/printer.cmx lib/pp.cmx 
 contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
 contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \
diff --git a/make.result b/make.result
index 9a2dbad074..9028fc423d 100644
--- a/make.result
+++ b/make.result
@@ -1 +1 @@
-Mon 20/02/2006 00:30: Success
+Tue 21/02/2006 00:30: Success