aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend2
-rw-r--r--.depend.camlp41
2 files changed, 3 insertions, 0 deletions
diff --git a/.depend b/.depend
index b9bd659ef7..2cfda23c9b 100644
--- a/.depend
+++ b/.depend
@@ -3316,6 +3316,8 @@ contrib/interface/debug_tac.cmo: parsing/grammar.cma
contrib/interface/debug_tac.cmx: parsing/grammar.cma
contrib/interface/centaur.cmo: parsing/grammar.cma
contrib/interface/centaur.cmx: parsing/grammar.cma
+contrib/interface/explication.cmo:
+contrib/interface/explication.cmx:
parsing/lexer.cmo:
parsing/lexer.cmx:
parsing/q_util.cmo:
diff --git a/.depend.camlp4 b/.depend.camlp4
index bbdeaa7bea..d82fe11913 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -17,6 +17,7 @@ contrib/funind/tacinv.ml: parsing/grammar.cma
contrib/first-order/g_ground.ml: parsing/grammar.cma
contrib/interface/debug_tac.ml: parsing/grammar.cma
contrib/interface/centaur.ml: parsing/grammar.cma
+contrib/interface/explication.ml:
parsing/lexer.ml:
parsing/q_util.ml:
parsing/q_coqast.ml: