diff options
| author | filliatr | 1999-12-03 17:32:44 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-03 17:32:44 +0000 |
| commit | f1d434e2044840f1e3ee7dc7d359a1f25846881e (patch) | |
| tree | 96edaa9c81fe15d2dc8eafcf7c4a3a3dd317b44f /Makefile | |
| parent | 4a2b9073e61de1ab000b26652d94e63b382ce7d2 (diff) | |
compilation native
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 11 insertions, 1 deletions
@@ -85,6 +85,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/extend.cmo parsing/termast.cmo \ parsing/esyntax.cmo parsing/printer.cmo parsing/pretty.cmo \ parsing/astterm.cmo parsing/egrammar.cmo +ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo PROOFS=proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ @@ -107,7 +108,7 @@ CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ $(PROOFS) $(TACTICS) $(TOPLEVEL) -CMX=$(CMO:.cmo=.cmx) +CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) ########################################################################### # Main targets @@ -255,6 +256,15 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma beforedepend:: $(GRAMMARCMO) +# toplevel/mltop.ml4 (ifdef Opt) + +CAMLP4IFDEF=camlp4o pa_ifdef.cmo + +toplevel/mltop.cmo: toplevel/mltop.ml4 + $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -DByte -impl" -impl $< +toplevel/mltop.cmx: toplevel/mltop.ml4 + $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< + ########################################################################### # Default rules ########################################################################### |