aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-09-06 15:15:38 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-09-06 15:15:38 +0000
commit16468065acddd4b37bf22f221e6eff604b1c381d (patch)
tree30b4b77664e4ce01f9c64c7fada6075855028007 /Makefile
parent136cb0538a61792ed8caca9969c8052cc9b42071 (diff)
mise en place repertoire test-suite/, toplevel/, parsing/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@39 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile19
1 files changed, 16 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index e062d3997..9b2060b3a 100644
--- a/Makefile
+++ b/Makefile
@@ -20,6 +20,8 @@ INCLUDES=-I config -I lib -I kernel -I library
# Objects files
+CLIBS=unix.cma
+
CONFIG=config/coq_config.cmo
LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \
@@ -35,13 +37,21 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
LIBRARY=library/libobject.cmo library/summary.cmo
-OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY)
+PARSING=parsing/lexer.cmo
+
+OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING)
# Targets
world: $(OBJS)
#$(OCAMLC) -o coqtop.byte $(OBJS)
- ocamlmktop -o coqtop $(OBJS)
+ ocamlmktop -o coqtop -custom $(CLIBS) $(OBJS) $(OSDEPLIBS)
+
+MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) $(PARSING) toplevel/minicoq.cmo
+
+minicoq: $(OBJS) $(MINICOQOBJS)
+ $(OCAMLC) -o minicoq -custom $(CLIBS) $(OBJS) $(MINICOQOBJS) \
+ $(OSDEPLIBS)
# Literate programming (with ocamlweb)
@@ -69,7 +79,7 @@ tags:
# Default rules
-.SUFFIXES: .ml .mli .cmo .cmi .cmx
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll
.ml.cmo:
$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -80,6 +90,9 @@ tags:
.ml.cmx:
$(OCAMLOPT) $(OPTFLAGS) -c $<
+.mll.ml:
+ ocamllex $<
+
# Cleaning
archclean::