diff options
Diffstat (limited to 'lib')
48 files changed, 416 insertions, 291 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index b16e60da5..7d9c528e7 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* The file format is a header diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 1ee51312d..efdd75fd3 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type aux_file diff --git a/lib/cAst.ml b/lib/cAst.ml index 301a6bac8..e1da072db 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** The ast type contains generic metadata for AST nodes. *) diff --git a/lib/cAst.mli b/lib/cAst.mli index 700a06ce8..8443b1af3 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** The ast type contains generic metadata for AST nodes *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index eaffc28ac..811fcf406 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) open Pp @@ -45,8 +47,6 @@ exception AlreadyDeclared of Pp.t (* for already declared Schemes *) let alreadydeclared pps = raise (AlreadyDeclared(pps)) exception Timeout -exception Drop -exception Quit let handle_stack = ref [] @@ -124,7 +124,7 @@ end let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ - | Timeout | Drop | Quit -> false + | Timeout -> false | Invalid_argument "equal: functional value" -> false | _ -> true [@@@ocaml.warning "+52"] diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 6fcc97a91..4e2fe7621 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) (** This modules implements basic manipulations of errors for use throughout Coq's code. *) @@ -51,8 +53,6 @@ val invalid_arg : ?loc:Loc.t -> string -> 'a val todo : string -> unit exception Timeout -exception Drop -exception Quit (** [register_handler h] registers [h] as a handler. When an expression is printed with [print e], it diff --git a/lib/cProfile.ml b/lib/cProfile.ml index 0bc226a45..07a114502 100644 --- a/lib/cProfile.ml +++ b/lib/cProfile.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) let word_length = Sys.word_size / 8 diff --git a/lib/cProfile.mli b/lib/cProfile.mli index cae4397a1..764faf8d1 100644 --- a/lib/cProfile.mli +++ b/lib/cProfile.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {6 This program is a small time and allocation profiler for Objective Caml } *) diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 3699b1c61..92c86eaea 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index ba152a19b..fa96b18c8 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type status = Disabled | Enabled | AsError diff --git a/lib/control.ml b/lib/control.ml index c6489938e..e67cd8b38 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*s interruption *) diff --git a/lib/control.mli b/lib/control.mli index 261b07693..415e05462 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Global control of Coq. *) diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index e6f1d7e06..d6c340f69 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -1,32 +1,39 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + type project = { project_file : string option; makefile : string option; install_kind : install option; use_ocamlopt : bool; - v_files : string list; - mli_files : string list; - ml4_files : string list; - ml_files : string list; - mllib_files : string list; - mlpack_files : string list; - - ml_includes : path list; - r_includes : (path * logic_path) list; - q_includes : (path * logic_path) list; - extra_args : string list; - defs : (string * string) list; - - extra_targets : extra_target list; - subdirs : string list; + v_files : string sourced list; + mli_files : string sourced list; + ml4_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; + + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -112,6 +119,7 @@ let exists_dir dir = let process_cmd_line orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in + let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in @@ -141,17 +149,17 @@ let process_cmd_line orig_dir proj args = aux { proj with install_kind = Some install } r | "-extra" :: target :: dependencies :: command :: r -> let tgt = { target; dependencies; phony = false; command } in - aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r | "-extra-phony" :: target :: dependencies :: command :: r -> let tgt = { target; dependencies; phony = true; command } in - aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r | "-Q" :: d :: lp :: r -> - aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r + aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r | "-I" :: d :: r -> - aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r + aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r | "-R" :: d :: lp :: r -> - aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r + aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r | "-f" :: file :: r -> if !parsing_project_file then @@ -176,20 +184,21 @@ let process_cmd_line orig_dir proj args = error "Option -o given more than once"; aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> - aux { proj with defs = proj.defs @ [v,def] } r + aux { proj with defs = proj.defs @ [sourced (v,def)] } r | "-arg" :: a :: r -> - aux { proj with extra_args = proj.extra_args @ [a] } r + aux { proj with extra_args = proj.extra_args @ [sourced a] } r | f :: r -> let f = CUnix.correct_path f orig_dir in let proj = - if exists_dir f then { proj with subdirs = proj.subdirs @ [f] } + if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } else match CUnix.get_extension f with - | ".v" -> { proj with v_files = proj.v_files @ [f] } - | ".ml" -> { proj with ml_files = proj.ml_files @ [f] } - | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] } - | ".mli" -> { proj with mli_files = proj.mli_files @ [f] } - | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] } - | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] } + | ".v" -> + { proj with v_files = proj.v_files @ [sourced f] } + | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } + | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } + | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } + | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } | _ -> raise (Parsing_error ("Unknown option "^f)) in aux proj r in @@ -213,16 +222,34 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; +let all_files { v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } = + v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + +let map_sourced_list f l = List.map (fun x -> f x.thing) l +;; + +let map_cmdline f l = CList.map_filter (function + | {thing=x; source=CmdLine} -> Some (f x) + | {source=ProjectFile} -> None) l + let coqtop_args_from_project { ml_includes; r_includes; q_includes; extra_args } = - let map = List.map in + let map = map_sourced_list in let args = map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ - [extra_args] in + [map (fun x -> x) extra_args] in List.flatten args ;; +let filter_cmdline l = CList.map_filter + (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None) + l +;; + +let forget_source {thing} = thing + (* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 810189450..5780bb5d7 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -1,36 +1,41 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) exception Parsing_error of string +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + type project = { project_file : string option; makefile : string option; install_kind : install option; use_ocamlopt : bool; - v_files : string list; - mli_files : string list; - ml4_files : string list; - ml_files : string list; - mllib_files : string list; - mlpack_files : string list; + v_files : string sourced list; + mli_files : string sourced list; + ml4_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; - ml_includes : path list; - r_includes : (path * logic_path) list; - q_includes : (path * logic_path) list; - extra_args : string list; - defs : (string * string) list; + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; (* deprecated in favor of a Makefile.local using :: rules *) - extra_targets : extra_target list; - subdirs : string list; - + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -50,3 +55,14 @@ val read_project_file : string -> project val coqtop_args_from_project : project -> string list val find_project_file : from:string -> projfile_name:string -> string option +val all_files : project -> string sourced list + +val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val filter_cmdline : 'a sourced list -> 'a list + +val forget_source : 'a sourced -> 'a diff --git a/lib/dAst.ml b/lib/dAst.ml index 0fe323d01..f34ab956a 100644 --- a/lib/dAst.ml +++ b/lib/dAst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CAst diff --git a/lib/dAst.mli b/lib/dAst.mli index 5b51677fc..28c78784e 100644 --- a/lib/dAst.mli +++ b/lib/dAst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Lazy AST node wrapper. Only used for [glob_constr] as of today. *) diff --git a/lib/envars.ml b/lib/envars.ml index 8ebf84057..be82bfe9b 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -155,23 +157,21 @@ let exe s = s ^ Coq_config.exec_extension let ocamlfind () = Coq_config.ocamlfind -(** {2 Camlp4 paths} *) +(** {2 Camlp5 paths} *) -let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) +let guess_camlp5bin () = which (user_path ()) (exe "camlp5") -let camlp4bin () = - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () +let camlp5bin () = + if !Flags.boot then Coq_config.camlp5bin else + try guess_camlp5bin () with Not_found -> - Coq_config.camlp4bin + Coq_config.camlp5bin -let camlp4 () = camlp4bin () / exe Coq_config.camlp4 - -let camlp4lib () = +let camlp5lib () = if !Flags.boot then - Coq_config.camlp4lib + Coq_config.camlp5lib else - let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in + let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" @@ -206,11 +206,10 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4; - fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o; - fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ()); - fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ()); - fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat; + fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; + fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ()); + fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ()); + fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); diff --git a/lib/envars.mli b/lib/envars.mli index 09f2b4ca1..66b86252c 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file provides a high-level interface to the environment variables @@ -56,14 +58,11 @@ val coqpath : string list (** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string -(** [camlp4bin ()] is the path to the camlp4 binary. *) -val camlp4bin : unit -> string +(** [camlp5bin ()] is the path to the camlp5 binary. *) +val camlp5bin : unit -> string -(** [camlp4lib ()] is the path to the camlp4 library. *) -val camlp4lib : unit -> string - -(** [camlp4 ()] is the camlp4 utility. *) -val camlp4 : unit -> string +(** [camlp5lib ()] is the path to the camlp5 library. *) +val camlp5lib : unit -> string (** Coq tries to honor the XDG Base Directory Specification to access the user's configuration files. diff --git a/lib/explore.ml b/lib/explore.ml index 7da077e96..4dc48ab66 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/lib/explore.mli b/lib/explore.mli index 5875246ff..528a1b97c 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {6 Search strategies. } *) diff --git a/lib/feedback.ml b/lib/feedback.ml index 1007582e0..cb8f8aad1 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Xml_datatype diff --git a/lib/feedback.mli b/lib/feedback.mli index 37f38c8ff..64fdf3724 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Xml_datatype diff --git a/lib/flags.ml b/lib/flags.ml index 01361dad5..8491873e0 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* If [restore] is false, whenever [f] modifies the ref, we will @@ -56,10 +58,8 @@ let in_toplevel = ref false let profile = false let ide_slave = ref false -let ideslave_coqtop_flags = ref None let raw_print = ref false - let univ_print = ref false let we_are_parsing = ref false @@ -69,17 +69,11 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current +type compat_version = V8_6 | V8_7 | Current let compat_version = ref Current let version_compare v1 v2 = match v1, v2 with - | VOld, VOld -> 0 - | VOld, _ -> -1 - | _, VOld -> 1 - | V8_5, V8_5 -> 0 - | V8_5, _ -> -1 - | _, V8_5 -> 1 | V8_6, V8_6 -> 0 | V8_6, _ -> -1 | _, V8_6 -> 1 @@ -92,8 +86,6 @@ let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function - | VOld -> "old" - | V8_5 -> "8.5" | V8_6 -> "8.6" | V8_7 -> "8.7" | Current -> "current" @@ -172,3 +164,7 @@ let profile_ltac_cutoff = ref 2.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode let get_dump_bytecode () = !dump_bytecode + +let dump_lambda = ref false +let set_dump_lambda = (:=) dump_lambda +let get_dump_lambda () = !dump_lambda diff --git a/lib/flags.mli b/lib/flags.mli index 33d281798..85aaf879f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Global options of the system. *) @@ -33,7 +35,6 @@ val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref -val ideslave_coqtop_flags : string option ref (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref @@ -44,7 +45,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current +type compat_version = V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool @@ -133,3 +134,8 @@ val profile_ltac_cutoff : float ref val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit val get_dump_bytecode : unit -> bool + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref +val set_dump_lambda : bool -> unit +val get_dump_lambda : unit -> bool diff --git a/lib/future.ml b/lib/future.ml index 09285ea27..7a5b6f699 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) let not_ready_msg = ref (fun name -> diff --git a/lib/future.mli b/lib/future.mli index 853f81cea..d9e8c87b2 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Futures: asynchronous computations. diff --git a/lib/genarg.ml b/lib/genarg.ml index a3bfb405c..209d1b271 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -172,19 +174,22 @@ sig val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option end +let get_arg_tag = function +| ExtraArg s -> s +| _ -> assert false + module Register (M : GenObj) = struct module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) let arg0_map = ref GenMap.empty - let register0 arg f = match arg with - | ExtraArg s -> + let register0 arg f = + let s = get_arg_tag arg in if GenMap.mem s !arg0_map then let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map - | _ -> assert false let get_obj0 name = try @@ -197,8 +202,6 @@ struct (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) - let obj t = match t with - | ExtraArg s -> get_obj0 s - | _ -> assert false + let obj t = get_obj0 @@ get_arg_tag t end diff --git a/lib/genarg.mli b/lib/genarg.mli index 7fa71299e..bb85f99e3 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Generic arguments used by the extension mechanisms of several Coq ASTs. *) @@ -157,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type This is boilerplate code used here and there in the code of Coq. *) +val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag +(** Works only on base objects (ExtraArg), otherwise fails badly. *) + module type GenObj = sig type ('raw, 'glb, 'top) obj diff --git a/lib/hook.ml b/lib/hook.ml index 14ca27bcf..1e2a2f279 100644 --- a/lib/hook.ml +++ b/lib/hook.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type 'a content = diff --git a/lib/hook.mli b/lib/hook.mli index df38abc53..67abd34dd 100644 --- a/lib/hook.mli +++ b/lib/hook.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module centralizes the notions of hooks. Hooks are pointers that are to diff --git a/lib/lib.mllib b/lib/lib.mllib index b2260ba09..089185942 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -15,7 +15,6 @@ CWarnings Rtree System Explore -RTree CProfile Future Spawn diff --git a/lib/loc.ml b/lib/loc.ml index 2cf4d3960..6f5283aab 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Locations management *) diff --git a/lib/loc.mli b/lib/loc.mli index 800940f21..813c45fbb 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {5 Basic types} *) @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* The different kinds of blocks are: diff --git a/lib/pp.mli b/lib/pp.mli index d9be1c5ce..f3a0a29b8 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Coq document type. *) diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 4358d6b2b..978b8b738 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type 'a getter = unit -> 'a diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index c262e50e5..ae0605cfb 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Remote counters are *global* counters for fresh ids. In the master/slave diff --git a/lib/rtree.ml b/lib/rtree.ml index 6d3875fac..0e371025e 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/lib/rtree.mli b/lib/rtree.mli index 1a916bbaf..8edfc3d37 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Type of regular tree with nodes labelled by values of type 'a diff --git a/lib/spawn.ml b/lib/spawn.ml index de31d87d0..6d2ad3787 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) let proto_version = 0 diff --git a/lib/spawn.mli b/lib/spawn.mli index fd2b92ae3..c7a56349c 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This module implements spawning/killing managed processes with a diff --git a/lib/stateid.ml b/lib/stateid.ml index 29f020071..a258d5052 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type t = int diff --git a/lib/stateid.mli b/lib/stateid.mli index d9e75f584..5d4b71a35 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type t diff --git a/lib/system.ml b/lib/system.ml index e56736eb1..dfede29e8 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* $Id$ *) @@ -54,7 +56,8 @@ let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) -let trust_file_cache = ref true +(** Don't trust in interactive mode (the default) *) +let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = diff --git a/lib/system.mli b/lib/system.mli index 0c0cc9fae..3349dfea3 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {5 Coqtop specific system utilities} *) diff --git a/lib/util.ml b/lib/util.ml index 6de012da0..7d7d380b2 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) (* Mapping under pairs *) diff --git a/lib/util.mli b/lib/util.mli index c54f5825c..1eb60f509 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module contains numerous utility functions on strings, lists, diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli index c55f8c2f3..19c046e95 100644 --- a/lib/xml_datatype.mli +++ b/lib/xml_datatype.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** ['a gxml] is the type for semi-structured documents. They generalize |