maj

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

1 files changed, 42 insertions, 42 deletions

diff --git a/.depend b/.depend
index 4ae979bef1..fa4ef78cc8 100644
--- a/.depend
+++ b/.depend
@@ -1294,19 +1294,19 @@ parsing/q_util.cmx: lib/util.cmx parsing/q_util.cmi
 parsing/search.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \
     kernel/term.cmi pretyping/rawterm.cmi parsing/printer.cmi lib/pp.cmi \
     pretyping/pattern.cmi library/nametab.cmi kernel/names.cmi \
-    library/nameops.cmi pretyping/matching.cmi library/library.cmi \
-    library/libobject.cmi library/libnames.cmi pretyping/inductiveops.cmi \
-    library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
-    library/declaremods.cmi library/declare.cmi kernel/declarations.cmi \
-    interp/coqlib.cmi parsing/coqast.cmi parsing/search.cmi 
+    library/nameops.cmi pretyping/matching.cmi library/libobject.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi library/global.cmi \
+    pretyping/evd.cmi kernel/environ.cmi library/declaremods.cmi \
+    library/declare.cmi kernel/declarations.cmi interp/coqlib.cmi \
+    parsing/coqast.cmi parsing/search.cmi 
 parsing/search.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
     kernel/term.cmx pretyping/rawterm.cmx parsing/printer.cmx lib/pp.cmx \
     pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \
-    library/nameops.cmx pretyping/matching.cmx library/library.cmx \
-    library/libobject.cmx library/libnames.cmx pretyping/inductiveops.cmx \
-    library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
-    library/declaremods.cmx library/declare.cmx kernel/declarations.cmx \
-    interp/coqlib.cmx parsing/coqast.cmx parsing/search.cmi 
+    library/nameops.cmx pretyping/matching.cmx library/libobject.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx library/global.cmx \
+    pretyping/evd.cmx kernel/environ.cmx library/declaremods.cmx \
+    library/declare.cmx kernel/declarations.cmx interp/coqlib.cmx \
+    parsing/coqast.cmx parsing/search.cmi 
 parsing/tacextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     parsing/q_util.cmi parsing/q_coqast.cmo lib/pp_control.cmi lib/pp.cmi \
     parsing/pcoq.cmi interp/genarg.cmi parsing/argextend.cmo 
@@ -2375,48 +2375,48 @@ toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
     interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \
     toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \
-    kernel/typeops.cmi interp/topconstr.cmi kernel/term.cmi \
-    tactics/tactics.cmi parsing/tactic_printer.cmi proofs/tactic_debug.cmi \
-    proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    lib/system.cmi interp/syntax_def.cmi library/states.cmi \
-    tactics/setoid_replace.cmi parsing/search.cmi kernel/safe_typing.cmi \
-    interp/reserve.cmi pretyping/reductionops.cmi proofs/redexpr.cmi \
-    pretyping/recordops.cmi toplevel/record.cmi pretyping/rawterm.cmi \
-    proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printmod.cmi \
-    parsing/printer.cmi pretyping/pretyping.cmi parsing/prettyp.cmi \
-    lib/pp_control.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \
-    interp/notation.cmi library/nametab.cmi kernel/names.cmi \
+    kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
+    kernel/term.cmi tactics/tactics.cmi parsing/tactic_printer.cmi \
+    proofs/tactic_debug.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
+    proofs/tacexpr.cmo lib/system.cmi interp/syntax_def.cmi \
+    library/states.cmi tactics/setoid_replace.cmi parsing/search.cmi \
+    kernel/safe_typing.cmi interp/reserve.cmi pretyping/reductionops.cmi \
+    proofs/redexpr.cmi pretyping/recordops.cmi toplevel/record.cmi \
+    pretyping/rawterm.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \
+    parsing/printmod.cmi parsing/printer.cmi pretyping/pretyping.cmi \
+    parsing/prettyp.cmi lib/pp_control.cmi lib/pp.cmi proofs/pfedit.cmi \
+    lib/options.cmi interp/notation.cmi library/nametab.cmi kernel/names.cmi \
     library/nameops.cmi interp/modintern.cmi toplevel/mltop.cmi \
     toplevel/metasyntax.cmi library/library.cmi library/libnames.cmi \
     library/lib.cmi pretyping/inductiveops.cmi library/impargs.cmi \
     library/goptions.cmi library/global.cmi pretyping/evd.cmi \
     pretyping/evarutil.cmi kernel/environ.cmi kernel/entries.cmi \
-    pretyping/detyping.cmi library/declaremods.cmi library/decl_kinds.cmo \
-    interp/constrintern.cmi interp/constrextern.cmi toplevel/command.cmi \
-    pretyping/classops.cmi toplevel/class.cmi tactics/autorewrite.cmi \
-    tactics/auto.cmi toplevel/vernacentries.cmi 
+    pretyping/detyping.cmi library/declaremods.cmi kernel/declarations.cmi \
+    library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \
+    toplevel/command.cmi pretyping/classops.cmi toplevel/class.cmi \
+    tactics/autorewrite.cmi tactics/auto.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: kernel/vm.cmx toplevel/vernacinterp.cmx \
     toplevel/vernacexpr.cmx kernel/vconv.cmx lib/util.cmx kernel/univ.cmx \
-    kernel/typeops.cmx interp/topconstr.cmx kernel/term.cmx \
-    tactics/tactics.cmx parsing/tactic_printer.cmx proofs/tactic_debug.cmx \
-    proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    lib/system.cmx interp/syntax_def.cmx library/states.cmx \
-    tactics/setoid_replace.cmx parsing/search.cmx kernel/safe_typing.cmx \
-    interp/reserve.cmx pretyping/reductionops.cmx proofs/redexpr.cmx \
-    pretyping/recordops.cmx toplevel/record.cmx pretyping/rawterm.cmx \
-    proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printmod.cmx \
-    parsing/printer.cmx pretyping/pretyping.cmx parsing/prettyp.cmx \
-    lib/pp_control.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \
-    interp/notation.cmx library/nametab.cmx kernel/names.cmx \
+    kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \
+    kernel/term.cmx tactics/tactics.cmx parsing/tactic_printer.cmx \
+    proofs/tactic_debug.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
+    proofs/tacexpr.cmx lib/system.cmx interp/syntax_def.cmx \
+    library/states.cmx tactics/setoid_replace.cmx parsing/search.cmx \
+    kernel/safe_typing.cmx interp/reserve.cmx pretyping/reductionops.cmx \
+    proofs/redexpr.cmx pretyping/recordops.cmx toplevel/record.cmx \
+    pretyping/rawterm.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \
+    parsing/printmod.cmx parsing/printer.cmx pretyping/pretyping.cmx \
+    parsing/prettyp.cmx lib/pp_control.cmx lib/pp.cmx proofs/pfedit.cmx \
+    lib/options.cmx interp/notation.cmx library/nametab.cmx kernel/names.cmx \
     library/nameops.cmx interp/modintern.cmx toplevel/mltop.cmx \
     toplevel/metasyntax.cmx library/library.cmx library/libnames.cmx \
     library/lib.cmx pretyping/inductiveops.cmx library/impargs.cmx \
     library/goptions.cmx library/global.cmx pretyping/evd.cmx \
     pretyping/evarutil.cmx kernel/environ.cmx kernel/entries.cmx \
-    pretyping/detyping.cmx library/declaremods.cmx library/decl_kinds.cmx \
-    interp/constrintern.cmx interp/constrextern.cmx toplevel/command.cmx \
-    pretyping/classops.cmx toplevel/class.cmx tactics/autorewrite.cmx \
-    tactics/auto.cmx toplevel/vernacentries.cmi 
+    pretyping/detyping.cmx library/declaremods.cmx kernel/declarations.cmx \
+    library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \
+    toplevel/command.cmx pretyping/classops.cmx toplevel/class.cmx \
+    tactics/autorewrite.cmx tactics/auto.cmx toplevel/vernacentries.cmi 
 toplevel/vernacexpr.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \
     pretyping/rawterm.cmi interp/ppextend.cmi library/nametab.cmi \
     kernel/names.cmi library/libnames.cmi library/goptions.cmi \
@@ -3405,10 +3405,10 @@ contrib/ring/ring.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
     interp/coqlib.cmx interp/constrintern.cmx kernel/closure.cmx 
 contrib/romega/const_omega.cmo: lib/util.cmi kernel/term.cmi lib/options.cmi \
     library/nametab.cmi kernel/names.cmi library/libnames.cmi \
-    library/global.cmi interp/coqlib.cmi lib/bigint.cmi 
+    interp/coqlib.cmi lib/bigint.cmi 
 contrib/romega/const_omega.cmx: lib/util.cmx kernel/term.cmx lib/options.cmx \
     library/nametab.cmx kernel/names.cmx library/libnames.cmx \
-    library/global.cmx interp/coqlib.cmx lib/bigint.cmx 
+    interp/coqlib.cmx lib/bigint.cmx 
 contrib/romega/g_romega.cmo: lib/util.cmi tactics/tacinterp.cmi \
     proofs/tacexpr.cmo contrib/romega/refl_omega.cmo proofs/refiner.cmi \
     parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \