diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-06 15:15:38 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-06 15:15:38 +0000 |
commit | 16468065acddd4b37bf22f221e6eff604b1c381d (patch) | |
tree | 30b4b77664e4ce01f9c64c7fada6075855028007 /Makefile | |
parent | 136cb0538a61792ed8caca9969c8052cc9b42071 (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-- | Makefile | 19 |
1 files changed, 16 insertions, 3 deletions
@@ -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:: |