maj

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

1 files changed, 12 insertions, 10 deletions

diff --git a/.depend b/.depend
index ba5503f71..426ec2332 100644
--- a/.depend
+++ b/.depend
@@ -545,8 +545,8 @@ interp/constrextern.cmx: pretyping/classops.cmx kernel/declarations.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: kernel/environ.cmi pretyping/evd.cmi \
-    library/global.cmi library/impargs.cmi library/lib.cmi \
+interp/constrintern.cmo: kernel/declarations.cmi kernel/environ.cmi \
+    pretyping/evd.cmi library/global.cmi library/impargs.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/pretype_errors.cmi pretyping/pretyping.cmi \
@@ -554,8 +554,8 @@ interp/constrintern.cmo: kernel/environ.cmi pretyping/evd.cmi \
     pretyping/retyping.cmi kernel/sign.cmi interp/symbols.cmi \
     interp/syntax_def.cmi kernel/term.cmi pretyping/termops.cmi \
     interp/topconstr.cmi lib/util.cmi interp/constrintern.cmi 
-interp/constrintern.cmx: kernel/environ.cmx pretyping/evd.cmx \
-    library/global.cmx library/impargs.cmx library/lib.cmx \
+interp/constrintern.cmx: kernel/declarations.cmx kernel/environ.cmx \
+    pretyping/evd.cmx library/global.cmx library/impargs.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/pretype_errors.cmx pretyping/pretyping.cmx \
@@ -911,12 +911,14 @@ parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx library/libnames.cmx \
     kernel/names.cmx lib/util.cmx parsing/coqast.cmi 
 parsing/egrammar.cmo: parsing/ast.cmi lib/bignat.cmi parsing/extend.cmi \
     interp/genarg.cmi parsing/lexer.cmi library/libnames.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi proofs/tacexpr.cmo interp/topconstr.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo parsing/egrammar.cmi 
+    lib/options.cmi parsing/pcoq.cmi lib/pp.cmi proofs/tacexpr.cmo \
+    interp/topconstr.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    parsing/egrammar.cmi 
 parsing/egrammar.cmx: parsing/ast.cmx lib/bignat.cmx parsing/extend.cmx \
     interp/genarg.cmx parsing/lexer.cmx library/libnames.cmx kernel/names.cmx \
-    parsing/pcoq.cmx lib/pp.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx parsing/egrammar.cmi 
+    lib/options.cmx parsing/pcoq.cmx lib/pp.cmx proofs/tacexpr.cmx \
+    interp/topconstr.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    parsing/egrammar.cmi 
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     lib/gmap.cmi lib/gmapl.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi interp/ppextend.cmi \
@@ -2809,12 +2811,12 @@ contrib/fourier/fourierR.cmo: proofs/clenv.cmi tactics/contradiction.cmi \
     interp/coqlib.cmi tactics/equality.cmi contrib/fourier/fourier.cmo \
     library/libnames.cmi library/library.cmi kernel/names.cmi \
     contrib/ring/ring.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi toplevel/vernacexpr.cmo 
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 contrib/fourier/fourierR.cmx: proofs/clenv.cmx tactics/contradiction.cmx \
     interp/coqlib.cmx tactics/equality.cmx contrib/fourier/fourier.cmx \
     library/libnames.cmx library/library.cmx kernel/names.cmx \
     contrib/ring/ring.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx toplevel/vernacexpr.cmx 
+    tactics/tactics.cmx kernel/term.cmx lib/util.cmx toplevel/vernacexpr.cmx 
 contrib/fourier/g_fourier.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
     contrib/fourier/fourierR.cmo lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
     parsing/pptactic.cmi proofs/refiner.cmi