aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2003-09-11 01:02:44 +0000
committerfilliatr2003-09-11 01:02:44 +0000
commita9513f52827e7cf2af6fed14330f51b885268d09 (patch)
tree1c951bd2b0b240b7f2b13c0f32eaacfa4d8dd2b0
parent5084d74089e68b2142c369d300e146ceefebaa3a (diff)
maj
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4351 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--.depend8
1 files changed, 4 insertions, 4 deletions
diff --git a/.depend b/.depend
index 38b051d7be..b91036c0d7 100644
--- a/.depend
+++ b/.depend
@@ -599,11 +599,11 @@ interp/ppextend.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
interp/ppextend.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
interp/ppextend.cmi
interp/reserve.cmo: library/lib.cmi library/libobject.cmi library/nameops.cmi \
- kernel/names.cmi pretyping/rawterm.cmi library/summary.cmi lib/util.cmi \
- interp/reserve.cmi
+ kernel/names.cmi lib/options.cmi pretyping/rawterm.cmi \
+ library/summary.cmi lib/util.cmi interp/reserve.cmi
interp/reserve.cmx: library/lib.cmx library/libobject.cmx library/nameops.cmx \
- kernel/names.cmx pretyping/rawterm.cmx library/summary.cmx lib/util.cmx \
- interp/reserve.cmi
+ kernel/names.cmx lib/options.cmx pretyping/rawterm.cmx \
+ library/summary.cmx lib/util.cmx interp/reserve.cmi
interp/symbols.cmo: lib/bignat.cmi pretyping/classops.cmi library/global.cmi \
lib/gmap.cmi lib/gmapl.cmi library/lib.cmi library/libnames.cmi \
library/libobject.cmi library/library.cmi kernel/names.cmi \