diff options
| author | filliatr | 1999-12-05 18:46:38 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-05 18:46:38 +0000 |
| commit | c70bdc0f7ddfca7055d1af4d81086485518056af (patch) | |
| tree | 081e2cb705e150d9b49b6cda91bb6e3ad58d67fa /Makefile | |
| parent | e22c71e0edeccc537bb8e584812ad0646ec0dd84 (diff) | |
premier debugage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 19 |
1 files changed, 17 insertions, 2 deletions
@@ -154,6 +154,13 @@ parsing: $(PARSING) pretyping: $(PRETYPING) toplevel: $(TOPLEVEL) +# states + +SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPMultipleCase.v + +states/barestate.coq: $(SYNTAXPP) coqtop.byte + ./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq + ########################################################################### # minicoq ########################################################################### @@ -256,7 +263,14 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma beforedepend:: $(GRAMMARCMO) -# toplevel/mltop.ml4 (ifdef Opt) +parsing/pcoq.ml: parsing/pcoq.ml4 + $(CAMLP4EXTEND) pr_o.cmo -impl $< -o $@ +parsing/extend.ml: parsing/extend.ml4 parsing/grammar.cma + $(CAMLP4GRAMMAR) pr_o.cmo -impl $< -o $@ + +beforedepend:: parsing/pcoq.ml parsing/extend.ml + +# toplevel/mltop.ml4 (ifdef Byte) CAMLP4IFDEF=camlp4o pa_ifdef.cmo @@ -303,6 +317,7 @@ archclean:: rm -f parsing/*.cmx parsing/*.[so] rm -f pretyping/*.cmx pretyping/*.[so] rm -f toplevel/*.cmx toplevel/*.[so] + rm -f coqtop coqtop.byte minicoq cleanall:: archclean rm -f *~ @@ -333,7 +348,7 @@ dependcamlp4: beforedepend rm -f .depend.camlp4 for f in */*.ml4; do \ file=`dirname $$f`/`basename $$f .ml4`; \ - camlp4o $(INCLUDES) pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \ + camlp4o $(INCLUDES) pa_ifdef.cmo pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \ ocamldep $(DEPFLAGS) $$file.ml >> .depend.camlp4; \ rm -f $$file.ml; \ done |