aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend2
1 files changed, 1 insertions, 1 deletions
diff --git a/.depend b/.depend
index b641d6d92c..21377c152e 100644
--- a/.depend
+++ b/.depend
@@ -58,7 +58,7 @@ kernel/safe_typing.cmi: kernel/cooking.cmi kernel/declarations.cmi \
kernel/sign.cmi: kernel/names.cmi kernel/term.cmi
kernel/subtyping.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/univ.cmi
-kernel/term.cmi: kernel/names.cmi kernel/univ.cmi
+kernel/term.cmi: kernel/esubst.cmi kernel/names.cmi kernel/univ.cmi
kernel/term_typing.cmi: kernel/cooking.cmi kernel/declarations.cmi \
kernel/entries.cmi kernel/environ.cmi kernel/inductive.cmi \
kernel/names.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi