diff options
| author | herbelin | 2000-11-28 15:37:31 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-28 15:37:31 +0000 |
| commit | 981942e985ee1a6243bb72b6a52900087abf277b (patch) | |
| tree | 29d72180ee3d27695062d43e8250ca1de53cba49 /Makefile | |
| parent | 85801f391cbfaec95f68e1bc1ff2c877bfa791ea (diff) | |
-I inutiles pour coqc et utilisation de -R theories (pour garder trace des noms de repertoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1002 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 21 |
1 files changed, 11 insertions, 10 deletions
@@ -29,9 +29,9 @@ noargument: # Compilation options ########################################################################### -LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ - -I proofs -I tactics -I pretyping -I parsing -I toplevel \ - -I contrib/omega -I contrib/ring -I contrib/xml +LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \ + -I proofs -I tactics -I pretyping -I parsing -I toplevel \ + -I contrib/omega -I contrib/ring -I contrib/xml INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG) @@ -44,11 +44,12 @@ OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' -COQINCLUDES=-I states -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/Wellfounded \ - -I theories/Reals +COQINCLUDES=-I states +# -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/Wellfounded \ +# -I theories/Reals ########################################################################### # Objects files @@ -223,7 +224,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic_TypeSyntax.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) - $(COQC) -$(BEST) -bindir bin -q -I theories/Init -is states/barestate.coq $< + $(COQC) -$(BEST) -bindir bin -q -R theories -is states/barestate.coq $< init: $(INITVO) @@ -234,7 +235,7 @@ tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP) - $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -I theories/Init -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq + $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: rm -f states/*~ states/*.coq |