diff options
| author | filliatr | 1999-12-13 15:23:16 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-13 15:23:16 +0000 |
| commit | d21d934c5ef9f47046a705eebd554e63f77b9e30 (patch) | |
| tree | c01d54e43f553ee1ebfd1fbffb3ee4d7e34c9832 /Makefile | |
| parent | decb8c16274487ce3cac1e7d5de529b46b6d68e3 (diff) | |
- états fabriqués avec -silent
- compilation theories avec -q
- correction but de tclORELSE qui doit maintenant rattraper aussi
TypeError et RefinerError
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@249 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -180,7 +180,7 @@ states: states/barestate.coq SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPCases.v states/barestate.coq: $(SYNTAXPP) coqtop.byte - ./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq + ./coqtop.byte -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq ########################################################################### # theories @@ -382,7 +382,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4 $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< .v.vo: - $(COQC) $(COQINCLUDES) $< + $(COQC) $(COQINCLUDES) -q $< .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile |