From 37f2f9762ff66e17d6d7d5aee8dae329d238de84 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 8 Nov 2003 11:25:18 +0000 Subject: Ajout option -impredicative-set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coq_makefile.ml4 | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index a71315ca8..66911531b 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) -- cgit v1.2.3