maj

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

1 files changed, 62 insertions, 58 deletions

diff --git a/.depend b/.depend
index 15d8f149a..958c64dc8 100644
--- a/.depend
+++ b/.depend
@@ -537,21 +537,21 @@ ide/preferences.cmx: ide/config_lexer.cmx ide/utils/configwin.cmx \
     ide/utils/editable_cells.cmx lib/util.cmx ide/preferences.cmi 
 ide/undo.cmo: ide/ideutils.cmi ide/undo.cmi 
 ide/undo.cmx: ide/ideutils.cmx ide/undo.cmi 
-interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
-    pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \
-    kernel/inductive.cmi library/lib.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi \
-    pretyping/recordops.cmi interp/reserve.cmi kernel/sign.cmi \
-    interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \
+interp/constrextern.cmo: pretyping/classops.cmi kernel/declarations.cmi \
+    library/declare.cmi pretyping/detyping.cmi kernel/environ.cmi \
+    library/global.cmi library/impargs.cmi kernel/inductive.cmi \
+    library/lib.cmi library/libnames.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi pretyping/recordops.cmi interp/reserve.cmi \
+    kernel/sign.cmi interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \
     interp/topconstr.cmi kernel/univ.cmi lib/util.cmi interp/constrextern.cmi 
-interp/constrextern.cmx: pretyping/classops.cmx library/declare.cmx \
-    pretyping/detyping.cmx kernel/environ.cmx library/impargs.cmx \
-    kernel/inductive.cmx library/lib.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    pretyping/pattern.cmx lib/pp.cmx pretyping/rawterm.cmx \
-    pretyping/recordops.cmx interp/reserve.cmx kernel/sign.cmx \
-    interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \
+interp/constrextern.cmx: pretyping/classops.cmx kernel/declarations.cmx \
+    library/declare.cmx pretyping/detyping.cmx kernel/environ.cmx \
+    library/global.cmx library/impargs.cmx kernel/inductive.cmx \
+    library/lib.cmx library/libnames.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
+    pretyping/rawterm.cmx pretyping/recordops.cmx interp/reserve.cmx \
+    kernel/sign.cmx interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.cmx kernel/univ.cmx lib/util.cmx interp/constrextern.cmi 
 interp/constrintern.cmo: lib/bignat.cmi library/declare.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
@@ -958,11 +958,11 @@ parsing/g_basevernac.cmx: parsing/ast.cmx interp/constrintern.cmx \
     interp/ppextend.cmx parsing/termast.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx 
 parsing/g_cases.cmo: parsing/g_constr.cmo library/libnames.cmi \
-    parsing/pcoq.cmi lib/pp.cmi kernel/term.cmi interp/topconstr.cmi \
-    lib/util.cmi 
+    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi kernel/term.cmi \
+    interp/topconstr.cmi lib/util.cmi 
 parsing/g_cases.cmx: parsing/g_constr.cmx library/libnames.cmx \
-    parsing/pcoq.cmx lib/pp.cmx kernel/term.cmx interp/topconstr.cmx \
-    lib/util.cmx 
+    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx kernel/term.cmx \
+    interp/topconstr.cmx lib/util.cmx 
 parsing/g_constr.cmo: parsing/lexer.cmi library/libnames.cmi kernel/names.cmi \
     pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
     kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
@@ -1123,8 +1123,8 @@ parsing/g_zsyntaxnew.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
     parsing/extend.cmx library/libnames.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx interp/topconstr.cmx \
     lib/util.cmx parsing/g_zsyntaxnew.cmi 
-parsing/lexer.cmo: lib/options.cmi lib/pp.cmi parsing/lexer.cmi 
-parsing/lexer.cmx: lib/options.cmx lib/pp.cmx parsing/lexer.cmi 
+parsing/lexer.cmo: lib/pp.cmi parsing/lexer.cmi 
+parsing/lexer.cmx: lib/pp.cmx parsing/lexer.cmi 
 parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi library/decl_kinds.cmo \
     parsing/extend.cmi interp/genarg.cmi parsing/lexer.cmi \
     library/libnames.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
@@ -1304,14 +1304,14 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
 pretyping/detyping.cmo: kernel/declarations.cmi library/declare.cmi \
     kernel/environ.cmi library/global.cmi library/goptions.cmi \
     kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
     pretyping/termops.cmi kernel/univ.cmi lib/util.cmi pretyping/detyping.cmi 
 pretyping/detyping.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/environ.cmx library/global.cmx library/goptions.cmx \
     kernel/inductive.cmx pretyping/inductiveops.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx \
     pretyping/termops.cmx kernel/univ.cmx lib/util.cmx pretyping/detyping.cmi 
 pretyping/evarconv.cmo: pretyping/classops.cmi kernel/closure.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -1402,22 +1402,24 @@ pretyping/pretype_errors.cmx: kernel/environ.cmx pretyping/evd.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \
     pretyping/pretype_errors.cmi 
 pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
-    pretyping/coercion.cmi kernel/declarations.cmi lib/dyn.cmi \
-    kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \
-    pretyping/evd.cmi pretyping/indrec.cmi kernel/inductive.cmi \
-    pretyping/inductiveops.cmi pretyping/instantiate.cmi library/libnames.cmi \
-    kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
+    pretyping/coercion.cmi kernel/declarations.cmi pretyping/detyping.cmi \
+    lib/dyn.cmi kernel/environ.cmi pretyping/evarconv.cmi \
+    pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
+    pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
+    pretyping/instantiate.cmi library/libnames.cmi library/nameops.cmi \
+    kernel/names.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
     pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
     kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \
     kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/pretyping.cmi 
 pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
-    pretyping/coercion.cmx kernel/declarations.cmx lib/dyn.cmx \
-    kernel/environ.cmx pretyping/evarconv.cmx pretyping/evarutil.cmx \
-    pretyping/evd.cmx pretyping/indrec.cmx kernel/inductive.cmx \
-    pretyping/inductiveops.cmx pretyping/instantiate.cmx library/libnames.cmx \
-    kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
+    pretyping/coercion.cmx kernel/declarations.cmx pretyping/detyping.cmx \
+    lib/dyn.cmx kernel/environ.cmx pretyping/evarconv.cmx \
+    pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
+    pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
+    pretyping/instantiate.cmx library/libnames.cmx library/nameops.cmx \
+    kernel/names.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx pretyping/rawterm.cmx \
     pretyping/recordops.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
@@ -2292,7 +2294,7 @@ translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
-    interp/ppextend.cmi pretyping/rawterm.cmi interp/reserve.cmi \
+    interp/ppextend.cmi pretyping/pretyping.cmi pretyping/rawterm.cmi \
     interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \
     interp/topconstr.cmi lib/util.cmi translate/ppconstrnew.cmi 
 translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \
@@ -2300,44 +2302,46 @@ translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \
     pretyping/evd.cmx interp/genarg.cmx library/global.cmx \
     library/libnames.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
-    interp/ppextend.cmx pretyping/rawterm.cmx interp/reserve.cmx \
+    interp/ppextend.cmx pretyping/pretyping.cmx pretyping/rawterm.cmx \
     interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.cmx lib/util.cmx translate/ppconstrnew.cmi 
 translate/pptacticnew.cmo: kernel/closure.cmi interp/constrextern.cmi \
     lib/dyn.cmi parsing/egrammar.cmi kernel/environ.cmi parsing/extend.cmi \
     interp/genarg.cmi library/global.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    lib/pp.cmi translate/ppconstrnew.cmi interp/ppextend.cmi \
-    parsing/pptactic.cmi parsing/printer.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo pretyping/termops.cmi interp/topconstr.cmi \
-    lib/util.cmi translate/pptacticnew.cmi 
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    translate/ppconstrnew.cmi interp/ppextend.cmi parsing/pptactic.cmi \
+    parsing/printer.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
+    pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \
+    translate/pptacticnew.cmi 
 translate/pptacticnew.cmx: kernel/closure.cmx interp/constrextern.cmx \
     lib/dyn.cmx parsing/egrammar.cmx kernel/environ.cmx parsing/extend.cmx \
     interp/genarg.cmx library/global.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    lib/pp.cmx translate/ppconstrnew.cmx interp/ppextend.cmx \
-    parsing/pptactic.cmx parsing/printer.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx pretyping/termops.cmx interp/topconstr.cmx \
-    lib/util.cmx translate/pptacticnew.cmi 
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    translate/ppconstrnew.cmx interp/ppextend.cmx parsing/pptactic.cmx \
+    parsing/printer.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
+    pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \
+    translate/pptacticnew.cmi 
 translate/ppvernacnew.cmo: parsing/ast.cmi interp/constrextern.cmi \
-    interp/constrintern.cmi parsing/coqast.cmi library/decl_kinds.cmo \
-    parsing/egrammar.cmi pretyping/evd.cmi parsing/extend.cmi \
-    interp/genarg.cmi library/global.cmi library/goptions.cmi \
-    library/impargs.cmi library/libnames.cmi toplevel/metasyntax.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi translate/ppconstrnew.cmi \
+    interp/constrintern.cmi parsing/coqast.cmi interp/coqlib.cmi \
+    library/decl_kinds.cmo parsing/egrammar.cmi kernel/environ.cmi \
+    pretyping/evd.cmi parsing/extend.cmi interp/genarg.cmi library/global.cmi \
+    library/goptions.cmi library/impargs.cmi library/lib.cmi \
+    library/libnames.cmi toplevel/metasyntax.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \
+    proofs/pfedit.cmi lib/pp.cmi translate/ppconstrnew.cmi \
     interp/ppextend.cmi parsing/pptactic.cmi translate/pptacticnew.cmi \
     pretyping/rawterm.cmi interp/reserve.cmi proofs/tacexpr.cmo \
     tactics/tacinterp.cmi kernel/term.cmi pretyping/termops.cmi \
     interp/topconstr.cmi lib/util.cmi toplevel/vernacexpr.cmo \
     translate/ppvernacnew.cmi 
 translate/ppvernacnew.cmx: parsing/ast.cmx interp/constrextern.cmx \
-    interp/constrintern.cmx parsing/coqast.cmx library/decl_kinds.cmx \
-    parsing/egrammar.cmx pretyping/evd.cmx parsing/extend.cmx \
-    interp/genarg.cmx library/global.cmx library/goptions.cmx \
-    library/impargs.cmx library/libnames.cmx toplevel/metasyntax.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx translate/ppconstrnew.cmx \
+    interp/constrintern.cmx parsing/coqast.cmx interp/coqlib.cmx \
+    library/decl_kinds.cmx parsing/egrammar.cmx kernel/environ.cmx \
+    pretyping/evd.cmx parsing/extend.cmx interp/genarg.cmx library/global.cmx \
+    library/goptions.cmx library/impargs.cmx library/lib.cmx \
+    library/libnames.cmx toplevel/metasyntax.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \
+    proofs/pfedit.cmx lib/pp.cmx translate/ppconstrnew.cmx \
     interp/ppextend.cmx parsing/pptactic.cmx translate/pptacticnew.cmx \
     pretyping/rawterm.cmx interp/reserve.cmx proofs/tacexpr.cmx \
     tactics/tacinterp.cmx kernel/term.cmx pretyping/termops.cmx \