diff options
| -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) |