summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml2
-rw-r--r--lib/bigint.mli2
-rw-r--r--lib/compat.ml42
-rw-r--r--lib/dnet.ml2
-rw-r--r--lib/dnet.mli2
-rw-r--r--lib/dyn.ml2
-rw-r--r--lib/dyn.mli2
-rw-r--r--lib/envars.ml28
-rw-r--r--lib/envars.mli2
-rw-r--r--lib/explore.ml2
-rw-r--r--lib/explore.mli2
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--lib/gmap.ml2
-rw-r--r--lib/gmap.mli2
-rw-r--r--lib/gmapl.ml2
-rw-r--r--lib/gmapl.mli2
-rw-r--r--lib/hashcons.ml2
-rw-r--r--lib/hashcons.mli2
-rw-r--r--lib/hashtbl_alt.ml2
-rw-r--r--lib/hashtbl_alt.mli2
-rw-r--r--lib/heap.ml2
-rw-r--r--lib/heap.mli2
-rw-r--r--lib/option.ml2
-rw-r--r--lib/option.mli2
-rw-r--r--lib/pp.ml42
-rw-r--r--lib/pp.mli2
-rw-r--r--lib/pp_control.ml2
-rw-r--r--lib/pp_control.mli2
-rw-r--r--lib/profile.ml2
-rw-r--r--lib/profile.mli2
-rw-r--r--lib/rtree.ml2
-rw-r--r--lib/rtree.mli2
-rw-r--r--lib/system.ml2
-rw-r--r--lib/system.mli2
-rw-r--r--lib/tries.ml2
-rw-r--r--lib/unionfind.ml2
-rw-r--r--lib/unionfind.mli2
-rw-r--r--lib/util.mli2
39 files changed, 51 insertions, 53 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 9185ba64..42a71f83 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 754f10d6..dd2cdea6 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index a428ec10..73cbc6d6 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/dnet.ml b/lib/dnet.ml
index 0562cc40..7f9bd949 100644
--- a/lib/dnet.ml
+++ b/lib/dnet.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/dnet.mli b/lib/dnet.mli
index 7ce43bd5..826e120a 100644
--- a/lib/dnet.mli
+++ b/lib/dnet.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index b795a4b4..e756297f 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 9173e810..3ddde2b6 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/envars.ml b/lib/envars.ml
index c672d30c..3040dd41 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,6 +9,8 @@
(* This file gathers environment variables needed by Coq to run (such
as coqlib) *)
+let (//) s1 s2 = s1 ^ "/" ^ s2
+
let coqbin =
System.canonical_path_name (Filename.dirname Sys.executable_name)
@@ -27,8 +29,8 @@ let exe s = s ^ Coq_config.exec_extension
let reldir instdir testfile oth =
let rpath = if Coq_config.local then [] else instdir in
- let out = List.fold_left Filename.concat coqroot rpath in
- if Sys.file_exists (Filename.concat out testfile) then out else oth ()
+ let out = List.fold_left (//) coqroot rpath in
+ if Sys.file_exists (out//testfile) then out else oth ()
let guess_coqlib () =
let file = "states/initial.coq" in
@@ -38,7 +40,7 @@ let guess_coqlib () =
| Some coqlib -> coqlib
| None -> coqroot
in
- if Sys.file_exists (Filename.concat coqlib file)
+ if Sys.file_exists (coqlib//file)
then coqlib
else Util.error "cannot guess a path for Coq libraries; please use -coqlib option")
@@ -54,18 +56,14 @@ let path_to_list p =
Util.split_string_at sep p
let xdg_data_home =
- Filename.concat
- (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share"))
- "coq"
+ (System.getenv_else "XDG_DATA_HOME" (System.home//".local/share"))//"coq"
let xdg_config_home =
- Filename.concat
- (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config"))
- "coq"
+ (System.getenv_else "XDG_CONFIG_HOME" (System.home//".config"))//"coq"
let xdg_data_dirs =
(try
- List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
+ List.map (fun dir -> dir//"coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
with Not_found -> ["/usr/local/share/coq";"/usr/share/coq"])
@ (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir])
@@ -84,7 +82,7 @@ let rec which l f =
match l with
| [] -> raise Not_found
| p :: tl ->
- if Sys.file_exists (Filename.concat p f)
+ if Sys.file_exists (p//f)
then p
else which tl f
@@ -108,7 +106,7 @@ let camllib () =
then Coq_config.camllib
else
let camlbin = camlbin () in
- let com = (Filename.concat camlbin "ocamlc") ^ " -where" in
+ let com = (camlbin//"ocamlc") ^ " -where" in
let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
Util.strip res
@@ -117,7 +115,7 @@ let camlp4bin () =
if !Flags.boot then Coq_config.camlp4bin else
try guess_camlp4bin () with e when e <> Sys.Break ->
let cb = camlbin () in
- if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb
+ if Sys.file_exists (cb//(exe Coq_config.camlp4)) then cb
else Coq_config.camlp4bin
let camlp4lib () =
@@ -125,7 +123,7 @@ let camlp4lib () =
then Coq_config.camlp4lib
else
let camlp4bin = camlp4bin () in
- let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
+ let com = (camlp4bin//Coq_config.camlp4) ^ " -where" in
let ex,res = System.run_command (fun x -> x) (fun _ -> ()) com in
match ex with
|Unix.WEXITED 0 -> Util.strip res
diff --git a/lib/envars.mli b/lib/envars.mli
index 9ec170db..023b54c0 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/explore.ml b/lib/explore.ml
index 1c8776a4..31a96774 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/explore.mli b/lib/explore.mli
index 7190d5e3..aaf11229 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/flags.ml b/lib/flags.ml
index 32c68b25..f6d98ba5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/flags.mli b/lib/flags.mli
index eb53f1a2..ede4629c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 08c99daf..e1c68da0 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 06fbd638..c2fb7d26 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 8c61d6eb..987ff9af 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index 5e772088..5b81459b 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 5f4738dc..d310713e 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index b4a9da2f..d2aa6462 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/hashtbl_alt.ml b/lib/hashtbl_alt.ml
index bb2252da..14b439ec 100644
--- a/lib/hashtbl_alt.ml
+++ b/lib/hashtbl_alt.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/hashtbl_alt.mli b/lib/hashtbl_alt.mli
index 7a1dcd57..f14fd90f 100644
--- a/lib/hashtbl_alt.mli
+++ b/lib/hashtbl_alt.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/heap.ml b/lib/heap.ml
index 4f0a65a6..372cecfc 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/heap.mli b/lib/heap.mli
index c2bd95ae..ee86e814 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/option.ml b/lib/option.ml
index 0500becc..d6df7063 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/option.mli b/lib/option.mli
index f8aeecc5..121d6500 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index d3b402e3..f13a3d16 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/pp.mli b/lib/pp.mli
index f292dedf..695bcbc0 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index dce42e29..94fdb881 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index f887e9ec..2c2d00f3 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/profile.ml b/lib/profile.ml
index 39e08721..0e4c2ebf 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/profile.mli b/lib/profile.mli
index a67622fd..1e45ceed 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 9ef7f313..cfac6aa4 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 7bfac2d4..8b12fee1 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/system.ml b/lib/system.ml
index ae637708..8f436366 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/system.mli b/lib/system.mli
index d8420e7d..b56e65a4 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/tries.ml b/lib/tries.ml
index 90d23bf1..60b466b7 100644
--- a/lib/tries.ml
+++ b/lib/tries.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/unionfind.ml b/lib/unionfind.ml
index 38ab0ffa..300e8b0e 100644
--- a/lib/unionfind.ml
+++ b/lib/unionfind.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/unionfind.mli b/lib/unionfind.mli
index 18468661..0db9ff08 100644
--- a/lib/unionfind.mli
+++ b/lib/unionfind.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/util.mli b/lib/util.mli
index 05d499cb..530e838a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 05:23:31 +0000