diff options
| author | herbelin | 2003-11-08 11:25:18 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-08 11:25:18 +0000 |
| commit | 37f2f9762ff66e17d6d7d5aee8dae329d238de84 (patch) | |
| tree | 232d76c579d598853f648e471fcea9a45c33fe14 | |
| parent | a98cbb0391769b2904a8127d73cbb731521e8fce (diff) | |
Ajout option -impredicative-set
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | tools/coq_makefile.ml4 | 7 |
2 files changed, 7 insertions, 2 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index d35141f979..67fd50e8ca 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -137,7 +137,7 @@ let parse_args () = | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate"|"strict-implicit" - |"-dont-load-proofs" as o) :: rem -> + |"-dont-load-proofs"|"-impredicative-set" as o) :: rem -> parse (cfiles,o::args) rem | ("-v"|"--version") :: _ -> Usage.version () diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index a71315ca80..66911531bc 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -28,6 +28,7 @@ let some_vfile = ref false let some_mlfile = ref false let opt = ref "-opt" +let impredicative_set = ref false let print x = output_string !output_channel x let printf x = Printf.fprintf !output_channel x @@ -71,6 +72,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom [VARIABLE = value]: Add the variable definition \"VARIABLE=value\" [-byte]: compile with byte-code version of coq [-opt]: compile with native-code version of coq +[-impredicative-set]: compile with option -impredicative-set of coq [-f file]: take the contents of file as arguments [-o file]: output should go in file file [-h]: print this usage summary @@ -184,7 +186,8 @@ let variables l = print "override OPT=-byte\n" else print "OPT=\n"; - print "COQFLAGS=-q $(OPT) $(COQLIBS) $(COQ_XML)\n"; + if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; + print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQC=$(COQBIN)coqc\n"; print "GALLINA=gallina\n"; print "COQDOC=coqdoc\n"; @@ -341,6 +344,8 @@ let rec process_cmd_line = function opt := "-byte"; process_cmd_line r | ("-full"|"-opt") :: r -> opt := "-opt"; process_cmd_line r + | "-impredicative-set" :: r -> + impredicative_set := true; process_cmd_line r | "-custom" :: com :: dependencies :: file :: r -> some_file := true; Special (file,dependencies,com) :: (process_cmd_line r) |