diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-27 08:46:13 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-27 08:46:13 +0000 |
| commit | 751620c70bd3a77ed8fde7cca9e3893f339643b3 (patch) | |
| tree | 517f1e98436989ba549f36f4c895624482e1419e /Makefile | |
| parent | fc6300ffd9d98da50b6302e11742ac29eb572366 (diff) | |
g_natsyntax et g_zsyntax maintenant toujours linkes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -44,7 +44,7 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE) -COQINCLUDES=-I parsing -I contrib/omega -I contrib/ring -I contrib/xml \ +COQINCLUDES=-I contrib/omega -I contrib/ring -I contrib/xml \ -I theories/Init -I theories/Logic -I theories/Arith \ -I theories/Bool -I theories/Zarith -I theories/Lists \ -I theories/Sets -I theories/Relations -I theories/Reals @@ -93,9 +93,10 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_vernac.cmo parsing/g_tactic.cmo \ parsing/g_constr.cmo parsing/g_cases.cmo \ parsing/extend.cmo parsing/esyntax.cmo \ - parsing/printer.cmo parsing/pretty.cmo parsing/egrammar.cmo + parsing/printer.cmo parsing/pretty.cmo parsing/egrammar.cmo \ + parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo -ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo +# ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ @@ -120,15 +121,15 @@ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/ring/quote.cmo contrib/ring/ring.cmo \ - contrib/xml/xml.cmo contrib/xml/cooking.cmo contrib/xml/xmlcommand.cmo \ - contrib/xml/xmlentries.cmo + contrib/xml/xml.cmo contrib/xml/cooking.cmo \ + contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS) $(CONTRIB) -CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) +CMX=$(CMO:.cmo=.cmx) ########################################################################### # Main targets (coqmktop, coqtop.opt, coqtop.byte) |