aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend4
-rw-r--r--make.result2
2 files changed, 3 insertions, 3 deletions
diff --git a/.depend b/.depend
index d634429755..3a4e17378d 100644
--- a/.depend
+++ b/.depend
@@ -2164,7 +2164,7 @@ toplevel/metasyntax.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
library/libobject.cmi library/libnames.cmi library/lib.cmi \
parsing/lexer.cmi library/global.cmi parsing/extend.cmi \
parsing/egrammar.cmi interp/constrintern.cmi pretyping/classops.cmi \
- toplevel/metasyntax.cmi
+ lib/bigint.cmi toplevel/metasyntax.cmi
toplevel/metasyntax.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
interp/topconstr.cmx tactics/tacinterp.cmx library/summary.cmx \
pretyping/rawterm.cmx parsing/pptactic.cmx interp/ppextend.cmx lib/pp.cmx \
@@ -2172,7 +2172,7 @@ toplevel/metasyntax.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
library/libobject.cmx library/libnames.cmx library/lib.cmx \
parsing/lexer.cmx library/global.cmx parsing/extend.cmx \
parsing/egrammar.cmx interp/constrintern.cmx pretyping/classops.cmx \
- toplevel/metasyntax.cmi
+ lib/bigint.cmx toplevel/metasyntax.cmi
toplevel/minicoq.cmo: lib/util.cmi kernel/type_errors.cmi kernel/term.cmi \
kernel/sign.cmi kernel/safe_typing.cmi lib/pp.cmi kernel/names.cmi \
kernel/inductive.cmi parsing/g_minicoq.cmi toplevel/fhimsg.cmi \
diff --git a/make.result b/make.result
index f6fa20f03d..f2f4ffb5ec 100644
--- a/make.result
+++ b/make.result
@@ -1 +1 @@
-Sun 08/01/2006 00:30: Success
+Mon 09/01/2006 00:30: Success