From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- tools/coqc.ml | 4 ++-- tools/coqdep.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'tools') diff --git a/tools/coqc.ml b/tools/coqc.ml index b12d48710f..552a943c8c 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -77,12 +77,12 @@ let parse_args () = | ("-v"|"--version") :: _ -> Usage.version 0 | ("-where") :: _ -> - Envars.set_coqlib (fun x -> x); + Envars.set_coqlib ~fail:(fun x -> x); print_endline (Envars.coqlib ()); exit 0 | ("-config" | "--config") :: _ -> - Envars.set_coqlib (fun x -> x); + Envars.set_coqlib ~fail:(fun x -> x); Usage.print_config (); exit 0 diff --git a/tools/coqdep.ml b/tools/coqdep.ml index a9f1b73765..1c1c1be6aa 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -502,7 +502,7 @@ let coqdep () = let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) - (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x))); + (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x))); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; -- cgit v1.2.3 From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- tools/coqdoc/output.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'tools') diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 853bc29aa4..235f2588c8 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -64,7 +64,6 @@ val keyword : string -> loc -> unit val ident : string -> loc option -> unit val sublexer : char -> loc -> unit val sublexer_in_doc : char -> unit -val initialize : unit -> unit val proofbox : unit -> unit -- cgit v1.2.3 From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Sat, 22 Apr 2017 12:55:46 +0200 Subject: Warning 29: non escaped end of line may be non portable --- tools/coq_makefile.ml | 116 +++++++++++++++++++++++++------------------------- 1 file changed, 58 insertions(+), 58 deletions(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ed89bda2cf..4875cb62bf 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -56,48 +56,48 @@ let lib_dirs = let usage () = - output_string stderr "Usage summary: - -coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}] - ... [any] ... [-extra[-phony] result dependencies command] - ... [-I dir] ... [-R physicalpath logicalpath] - ... [-Q physicalpath logicalpath] ... [VARIABLE = value] - ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] - [-h] [--help] - -[file.v]: Coq file to be compiled -[file.ml[i4]?]: Objective Caml file to be compiled -[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml - library/module -[any] : subdirectory that should be \"made\" and has a Makefile itself - to do so. Very fragile and discouraged. -[-extra result dependencies command]: add target \"result\" with command - \"command\" and dependencies \"dependencies\". If \"result\" is not - generic (do not contains a %), \"result\" is built by _make all_ and - deleted by _make clean_. -[-extra-phony result dependencies command]: add a PHONY target \"result\" - with command \"command\" and dependencies \"dependencies\". Note that - _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as - as a dependencies of an already defined target \"foo\". -[-I dir]: look for Objective Caml dependencies in \"dir\" -[-R physicalpath logicalpath]: look for Coq dependencies resursively - starting from \"physicalpath\". The logical path associated to the - physical path is \"logicalpath\". -[-Q physicalpath logicalpath]: look for Coq dependencies starting from - \"physicalpath\". The logical path associated to the physical path - is \"logicalpath\". -[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" -[-byte]: compile with byte-code version of coq -[-opt]: compile with native-code version of coq -[-arg opt]: send option \"opt\" to coqc -[-install opt]: where opt is \"user\" to force install into user directory, - \"none\" to build a makefile with no install target or - \"global\" to force install in $COQLIB directory -[-f file]: take the contents of file as arguments -[-o file]: output should go in file file - Output file outside the current directory is forbidden. -[-h]: print this usage summary -[--help]: equivalent to [-h]\n"; + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n\ +\n[file.v]: Coq file to be compiled\ +\n[file.ml[i4]?]: Objective Caml file to be compiled\ +\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ +\n library/module\ +\n[any] : subdirectory that should be \"made\" and has a Makefile itself\ +\n to do so. Very fragile and discouraged.\ +\n[-extra result dependencies command]: add target \"result\" with command\ +\n \"command\" and dependencies \"dependencies\". If \"result\" is not\ +\n generic (do not contains a %), \"result\" is built by _make all_ and\ +\n deleted by _make clean_.\ +\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\ +\n with command \"command\" and dependencies \"dependencies\". Note that\ +\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ +\n as a dependencies of an already defined target \"foo\".\ +\n[-I dir]: look for Objective Caml dependencies in \"dir\"\ +\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ +\n starting from \"physicalpath\". The logical path associated to the\ +\n physical path is \"logicalpath\".\ +\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ +\n \"physicalpath\". The logical path associated to the physical path\ +\n is \"logicalpath\".\ +\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\ +\n[-byte]: compile with byte-code version of coq\ +\n[-opt]: compile with native-code version of coq\ +\n[-arg opt]: send option \"opt\" to coqc\ +\n[-install opt]: where opt is \"user\" to force install into user directory,\ +\n \"none\" to build a makefile with no install target or\ +\n \"global\" to force install in $COQLIB directory\ +\n[-f file]: take the contents of file as arguments\ +\n[-o file]: output should go in file file\ +\n Output file outside the current directory is forbidden.\ +\n[-h]: print this usage summary\ +\n[--help]: equivalent to [-h]\n"; exit 1 let is_genrule r = (* generic rule (like bar%foo: ...) *) @@ -264,8 +264,8 @@ let where_put_doc = function then physical_dir_of_logical_dir pr else - let () = prerr_string "Warning: -Q options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n" in + let () = prerr_string ("Warning: -Q options don't have a correct common prefix," + ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in "$(INSTALLDEFAULTROOT)" |_,inc_i,((_,lp,_)::q as inc_r) -> let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in @@ -277,8 +277,8 @@ let where_put_doc = function then physical_dir_of_logical_dir pr else - let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n" in + let () = prerr_string ("Warning: -R/-Q options don't have a correct common prefix," + ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function @@ -518,8 +518,8 @@ let variables is_install opt (args,defs) = if !some_ml4file || !some_mlfile || !some_mlifile then begin print "COQSRCLIBS?=" ; List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ; - List.iter (fun c -> print " \\ - -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; + List.iter (fun c -> print " \\\ +\n -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n"; print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n"; @@ -529,8 +529,8 @@ let variables is_install opt (args,defs) = print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ - $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\\ +\n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () @@ -816,14 +816,14 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = let banner () = print (Printf.sprintf -"############################################################################# -## v # The Coq Proof Assistant ## -## flush stdout; eprintf "coqwc: %s\n" s; flush stderr +[@@@ocaml.warning "+52"] (*s Parsing of the command line. *) -- cgit v1.2.3 From 9ddfdab6a4715a08a78296bf8824d086f358bdc0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 14 May 2017 11:14:43 +0200 Subject: Dead code in coqdep. Was introduced in 5268efdef, reverted then readded in 1be9c4d. --- tools/coqdep_common.ml | 7 ------- tools/coqdep_common.mli | 3 --- 2 files changed, 10 deletions(-) (limited to 'tools') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0064aebdae..93b25e2ede 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -544,13 +544,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir = let add_rec_dir_import add_file phys_dir log_dir = add_directory true (add_file true) phys_dir log_dir -(** -R semantic but only on immediate capitalized subdirs *) - -let add_rec_uppercase_subdirs add_file phys_dir log_dir = - process_subdirectories (fun phys_dir f -> - add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f])) - phys_dir - (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = add_directory false add_caml_known phys_dir [] diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 633c474ada..10da0240dd 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -64,8 +64,5 @@ val add_rec_dir_no_import : val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val add_rec_uppercase_subdirs : - (bool -> string -> string list -> string -> unit) -> string -> string list -> unit - val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a -- cgit v1.2.3 From 3c0d8d08bda81b9fbd7210e4e352a08bbe8219e8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 17 May 2017 20:55:32 +0200 Subject: [vernac] Remove `Save.` command. It has been deprecated for a while in favor of `Qed`. --- tools/gallina-syntax.el | 4 +--- tools/gallina_lexer.mll | 1 - 2 files changed, 1 insertion(+), 4 deletions(-) (limited to 'tools') diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el index c25abece15..662762b08c 100644 --- a/tools/gallina-syntax.el +++ b/tools/gallina-syntax.el @@ -390,7 +390,7 @@ ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful + ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful ("Fact" "fct" "Fact # : #." t "Fact") ("Goal" nil "Goal #." t "Goal") ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") @@ -492,7 +492,6 @@ ("Require" nil "Require #." t "Require") ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Save" nil "Save." t "Save") ("Search" nil "Search #" nil "Search") ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") @@ -710,7 +709,6 @@ Used by `coq-goal-command-p'" (defvar coq-keywords-save-strict '("Defined" - "Save" "Qed" "End" "Admitted" diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll index 449efd57cd..432b18e645 100644 --- a/tools/gallina_lexer.mll +++ b/tools/gallina_lexer.mll @@ -105,7 +105,6 @@ and end_of_line = parse | _ { print (Lexing.lexeme lexbuf) } and skip_proof = parse - | "Save." { end_of_line lexbuf } | "Save" space { skip_until_point lexbuf } | "Qed." { end_of_line lexbuf } -- cgit v1.2.3