aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.camlp4
diff options
context:
space:
mode:
Diffstat (limited to '.depend.camlp4')
-rw-r--r--.depend.camlp41
1 files changed, 1 insertions, 0 deletions
diff --git a/.depend.camlp4 b/.depend.camlp4
index 9e69e8844..b29845a64 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -3,6 +3,7 @@ tactics/eqdecide.ml: parsing/grammar.cma
tactics/extraargs.ml: parsing/grammar.cma
tactics/extratactics.ml: parsing/grammar.cma
tactics/eauto.ml: parsing/grammar.cma
+toplevel/whelp.ml: parsing/grammar.cma
contrib/omega/g_omega.ml: parsing/grammar.cma
contrib/romega/g_romega.ml: parsing/grammar.cma
contrib/ring/g_quote.ml: parsing/grammar.cma