aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-20 18:10:57 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-20 18:10:57 +0000
commit1f96d480842a1206a9334d0c8b1b6cc4647066ef (patch)
tree9fc22a20d49bcefca1d863aee9d36c5fab03334f /Makefile
parent6c7f6fa6c215e5e28fcf23bf28ccb9db543709ba (diff)
Transparent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile14
1 files changed, 8 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index 5a46b9bcc..74b5227aa 100644
--- a/Makefile
+++ b/Makefile
@@ -71,7 +71,8 @@ CONFIG=config/coq_config.cmo
LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \
- lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo
+ lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
+ lib/predicate.cmo
KERNEL=kernel/names.cmo kernel/univ.cmo \
kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \
@@ -82,7 +83,8 @@ KERNEL=kernel/names.cmo kernel/univ.cmo \
LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \
library/lib.cmo library/goptions.cmo \
- library/global.cmo library/library.cmo library/states.cmo \
+ library/global.cmo library/opaque.cmo \
+ library/library.cmo library/states.cmo \
library/impargs.cmo library/indrec.cmo library/declare.cmo
PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \
@@ -147,8 +149,8 @@ INTERFACE=contrib/interface/vtp.cmo \
PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \
lib/util.cmo lib/dyn.cmo lib/gmap.cmo lib/gmapl.cmo \
- lib/hashcons.cmo lib/profile.cmo library/libobject.cmo \
- library/summary.cmo kernel/names.cmo \
+ lib/predicate.cmo lib/hashcons.cmo lib/profile.cmo \
+ library/libobject.cmo library/summary.cmo kernel/names.cmo \
parsing/lexer.cmo parsing/coqast.cmo \
parsing/pcoq.cmo parsing/ast.cmo \
parsing/g_prim.cmo parsing/g_basevernac.cmo \
@@ -162,7 +164,7 @@ PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \
kernel/instantiate.cmo kernel/closure.cmo kernel/reduction.cmo \
kernel/inductive.cmo kernel/type_errors.cmo kernel/typeops.cmo \
kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo \
- library/global.cmo \
+ library/global.cmo library/opaque.cmo \
library/library.cmo lib/options.cmo library/indrec.cmo \
library/impargs.cmo pretyping/retyping.cmo library/declare.cmo \
pretyping/cbv.cmo pretyping/tacred.cmo pretyping/classops.cmo \
@@ -702,7 +704,7 @@ ML4FILES += parsing/lexer.ml4 parsing/q_coqast.ml4 \
parsing/g_prim.ml4 parsing/pcoq.ml4
GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \
- lib/hashcons.cmo kernel/names.cmo \
+ lib/hashcons.cmo lib/predicate.cmo kernel/names.cmo \
parsing/coqast.cmo parsing/lexer.cmo \
parsing/pcoq.cmo parsing/q_coqast.cmo parsing/g_prim.cmo