diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-25 08:21:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-25 08:21:18 +0000 |
| commit | f3c6e557b2a8d53fefe7398294098028e33c9b09 (patch) | |
| tree | bae9f7b93ca9eb8beb69f857f6b91e06eaa4e540 | |
| parent | 5ca187d22a721677ff2bcbe4c4ebf0c9de6a8883 (diff) | |
Utilisation de -notop pour imposer l'absence de module toplevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7724 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -1094,13 +1094,13 @@ ALLOLDVO = $(OLDINITVO) $(OLDTHEORIESVO) $(OLDCONTRIBVO) SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v states7/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) - $(BESTCOQTOP) -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@ + $(BESTCOQTOP) -v7 -boot -batch -notop -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@ states7/initial.coq: states7/barestate.coq states7/MakeInitial.v $(OLDINITVO) $(BESTCOQTOP) - $(BOOTCOQTOP) -v7 -batch -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq + $(BOOTCOQTOP) -v7 -batch -notop -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq states/initial.coq: states/MakeInitial.v $(NEWINITVO) - $(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq + $(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq theories7/Init/%.vo: $(BESTCOQTOP) theories7/Init/%.v $(BOOTCOQTOP) $(TRANSLATE) -nois -compile theories7/Init/$* |