aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend2
1 files changed, 1 insertions, 1 deletions
diff --git a/.depend b/.depend
index 3dd95f717b..8f941435f5 100644
--- a/.depend
+++ b/.depend
@@ -391,7 +391,7 @@ contrib/extraction/ocaml.cmi: library/libnames.cmi \
contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
lib/pp.cmi
contrib/extraction/table.cmi: kernel/environ.cmi library/libnames.cmi \
- contrib/extraction/miniml.cmi kernel/names.cmi
+ contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi
contrib/funind/tacinvutils.cmi: interp/coqlib.cmi tactics/equality.cmi \
pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \
parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \