aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend.camlp42
-rw-r--r--make.result2
2 files changed, 3 insertions, 1 deletions
diff --git a/.depend.camlp4 b/.depend.camlp4
index f4531005a3..77abaeb73f 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -27,6 +27,8 @@ contrib/interface/centaur.ml: parsing/grammar.cma
parsing/lexer.ml:
parsing/pcoq.ml:
parsing/q_util.ml:
+parsing/q_coqast.ml:
+parsing/g_prim.ml:
parsing/g_minicoq.ml:
parsing/g_vernac.ml:
parsing/g_proofs.ml:
diff --git a/make.result b/make.result
index 21fdf9816c..e0818986fd 100644
--- a/make.result
+++ b/make.result
@@ -1 +1 @@
-Fri 30/12/2005 00:30: Success
+Sat 31/12/2005 00:30: Success