Merge branch 'trunk' into located_switch

9 files changed, 64 insertions, 76 deletions

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                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \\VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V%s ##
-#############################################################################
-
-" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
+"#############################################################################\
+\n##  v      #                   The Coq Proof Assistant                     ##\
+\n## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##\
+\n##   \\VV/  #                                                               ##\
+\n##    //   #  Makefile automagically generated by coq_makefile V%s ##\
+\n#############################################################################\
+\n\n"
+(Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
 
 let warning () =
   print "# WARNING\n#\n";
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;
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
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
 
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index b4fc738d0e..cd07d4216f 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -239,6 +239,7 @@ let process_channel ch =
   if !skip_header then read_header lb;
   spec lb
 
+[@@@ocaml.warning "-52"]
 let process_file f =
   try
     let ch = open_in f in
@@ -251,6 +252,7 @@ let process_file f =
 	flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
     | Sys_error s ->
 	flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+[@@@ocaml.warning "+52"]
 
 (*s Parsing of the command line. *)
 
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 }