aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
authorThéo Zimmermann2020-03-18 12:14:26 +0100
committerThéo Zimmermann2020-03-18 12:15:43 +0100
commita99776e10e0b2198d2b811ad82631111fb450f8a (patch)
tree2613f665dafdb34f34ebac4a9447208bbc35a8f6 /user-contrib
parenta33323d54cf78762f7ba1afc39a2f5a5ddb67a57 (diff)
Update headers in the whole code base.
Add headers to a few files which were missing them.
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/Array.v4
-rw-r--r--user-contrib/Ltac2/Bool.v4
-rw-r--r--user-contrib/Ltac2/Char.v4
-rw-r--r--user-contrib/Ltac2/Constr.v4
-rw-r--r--user-contrib/Ltac2/Control.v4
-rw-r--r--user-contrib/Ltac2/Env.v4
-rw-r--r--user-contrib/Ltac2/Fresh.v4
-rw-r--r--user-contrib/Ltac2/Ident.v4
-rw-r--r--user-contrib/Ltac2/Init.v4
-rw-r--r--user-contrib/Ltac2/Int.v4
-rw-r--r--user-contrib/Ltac2/List.v4
-rw-r--r--user-contrib/Ltac2/Ltac1.v4
-rw-r--r--user-contrib/Ltac2/Ltac2.v4
-rw-r--r--user-contrib/Ltac2/Message.v4
-rw-r--r--user-contrib/Ltac2/Notations.v4
-rw-r--r--user-contrib/Ltac2/Option.v4
-rw-r--r--user-contrib/Ltac2/Pattern.v4
-rw-r--r--user-contrib/Ltac2/Std.v4
-rw-r--r--user-contrib/Ltac2/String.v4
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg4
-rw-r--r--user-contrib/Ltac2/tac2core.ml4
-rw-r--r--user-contrib/Ltac2/tac2core.mli4
-rw-r--r--user-contrib/Ltac2/tac2dyn.ml4
-rw-r--r--user-contrib/Ltac2/tac2dyn.mli4
-rw-r--r--user-contrib/Ltac2/tac2entries.ml4
-rw-r--r--user-contrib/Ltac2/tac2entries.mli4
-rw-r--r--user-contrib/Ltac2/tac2env.ml4
-rw-r--r--user-contrib/Ltac2/tac2env.mli4
-rw-r--r--user-contrib/Ltac2/tac2expr.mli4
-rw-r--r--user-contrib/Ltac2/tac2extffi.ml4
-rw-r--r--user-contrib/Ltac2/tac2extffi.mli4
-rw-r--r--user-contrib/Ltac2/tac2ffi.ml4
-rw-r--r--user-contrib/Ltac2/tac2ffi.mli4
-rw-r--r--user-contrib/Ltac2/tac2intern.ml4
-rw-r--r--user-contrib/Ltac2/tac2intern.mli4
-rw-r--r--user-contrib/Ltac2/tac2interp.ml4
-rw-r--r--user-contrib/Ltac2/tac2interp.mli4
-rw-r--r--user-contrib/Ltac2/tac2match.ml4
-rw-r--r--user-contrib/Ltac2/tac2match.mli4
-rw-r--r--user-contrib/Ltac2/tac2print.ml4
-rw-r--r--user-contrib/Ltac2/tac2print.mli4
-rw-r--r--user-contrib/Ltac2/tac2qexpr.mli4
-rw-r--r--user-contrib/Ltac2/tac2quote.ml4
-rw-r--r--user-contrib/Ltac2/tac2quote.mli4
-rw-r--r--user-contrib/Ltac2/tac2stdlib.ml4
-rw-r--r--user-contrib/Ltac2/tac2stdlib.mli4
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml4
-rw-r--r--user-contrib/Ltac2/tac2tactics.mli4
-rw-r--r--user-contrib/Ltac2/tac2types.mli4
49 files changed, 98 insertions, 98 deletions
diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v
index ee3bf88647..5adba829c5 100644
--- a/user-contrib/Ltac2/Array.v
+++ b/user-contrib/Ltac2/Array.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v
index d808436e13..624097728e 100644
--- a/user-contrib/Ltac2/Bool.v
+++ b/user-contrib/Ltac2/Bool.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Char.v b/user-contrib/Ltac2/Char.v
index c48ea7be5c..dee104dcaf 100644
--- a/user-contrib/Ltac2/Char.v
+++ b/user-contrib/Ltac2/Char.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index a0b25afc37..c3343db149 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v
index 8f35e1a279..8b9d53a433 100644
--- a/user-contrib/Ltac2/Control.v
+++ b/user-contrib/Ltac2/Control.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Env.v b/user-contrib/Ltac2/Env.v
index 2cb8406618..d7c5e693f6 100644
--- a/user-contrib/Ltac2/Env.v
+++ b/user-contrib/Ltac2/Env.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Fresh.v b/user-contrib/Ltac2/Fresh.v
index 8872300ef9..548bf74a30 100644
--- a/user-contrib/Ltac2/Fresh.v
+++ b/user-contrib/Ltac2/Fresh.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Ident.v b/user-contrib/Ltac2/Ident.v
index 6b6041aff9..8ab56f8a96 100644
--- a/user-contrib/Ltac2/Ident.v
+++ b/user-contrib/Ltac2/Ident.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 65f0a362b1..271c3de556 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Int.v b/user-contrib/Ltac2/Int.v
index 60aafcd37d..edf88938f4 100644
--- a/user-contrib/Ltac2/Int.v
+++ b/user-contrib/Ltac2/Int.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v
index 89e14445ef..696bce5aff 100644
--- a/user-contrib/Ltac2/List.v
+++ b/user-contrib/Ltac2/List.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v
index d069150634..1a69708a7d 100644
--- a/user-contrib/Ltac2/Ltac1.v
+++ b/user-contrib/Ltac2/Ltac1.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Ltac2.v b/user-contrib/Ltac2/Ltac2.v
index 05bc36cbdc..d3bf3c10ea 100644
--- a/user-contrib/Ltac2/Ltac2.v
+++ b/user-contrib/Ltac2/Ltac2.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v
index 07a82f4d42..4a4d1d815c 100644
--- a/user-contrib/Ltac2/Message.v
+++ b/user-contrib/Ltac2/Message.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index d6bf4a28ba..373654e6db 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v
index 584d84ddb5..3223c1a570 100644
--- a/user-contrib/Ltac2/Option.v
+++ b/user-contrib/Ltac2/Option.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v
index b2cf97ea40..6e552120b1 100644
--- a/user-contrib/Ltac2/Pattern.v
+++ b/user-contrib/Ltac2/Pattern.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v
index af2249d058..b69a95faf3 100644
--- a/user-contrib/Ltac2/Std.v
+++ b/user-contrib/Ltac2/Std.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/String.v b/user-contrib/Ltac2/String.v
index 081025168d..731080b3a8 100644
--- a/user-contrib/Ltac2/String.v
+++ b/user-contrib/Ltac2/String.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index a0984aa2a9..5e04959e9a 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index f66ed7b4cf..864e2ebb0d 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2core.mli b/user-contrib/Ltac2/tac2core.mli
index eb66332936..e5523f8185 100644
--- a/user-contrib/Ltac2/tac2core.mli
+++ b/user-contrib/Ltac2/tac2core.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2dyn.ml b/user-contrib/Ltac2/tac2dyn.ml
index 32894f3643..a1e289d479 100644
--- a/user-contrib/Ltac2/tac2dyn.ml
+++ b/user-contrib/Ltac2/tac2dyn.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2dyn.mli b/user-contrib/Ltac2/tac2dyn.mli
index df4f003a1f..6d3b8d3424 100644
--- a/user-contrib/Ltac2/tac2dyn.mli
+++ b/user-contrib/Ltac2/tac2dyn.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 2820d3e3ad..e9945794d3 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index d96a6a95c5..fed43a4dd5 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index b0a910f10e..6c2133f8f2 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index effb9f705a..2468959810 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index b69b51b559..a95d8cc49f 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2extffi.ml b/user-contrib/Ltac2/tac2extffi.ml
index 7098ab4863..e0840b2680 100644
--- a/user-contrib/Ltac2/tac2extffi.ml
+++ b/user-contrib/Ltac2/tac2extffi.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2extffi.mli b/user-contrib/Ltac2/tac2extffi.mli
index 38b5b79084..3c0d967a69 100644
--- a/user-contrib/Ltac2/tac2extffi.mli
+++ b/user-contrib/Ltac2/tac2extffi.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index 9ae17bf9bc..58173faea6 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index ee13f00568..d84d2cabb7 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 4e39b21c53..a4f385d432 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index 5e282a386a..8b09ecbcf7 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml
index 3b5cdb79aa..54f2da0621 100644
--- a/user-contrib/Ltac2/tac2interp.ml
+++ b/user-contrib/Ltac2/tac2interp.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2interp.mli b/user-contrib/Ltac2/tac2interp.mli
index a186320668..e466c65224 100644
--- a/user-contrib/Ltac2/tac2interp.mli
+++ b/user-contrib/Ltac2/tac2interp.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml
index d18cfbf8ce..22f65507c1 100644
--- a/user-contrib/Ltac2/tac2match.ml
+++ b/user-contrib/Ltac2/tac2match.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2match.mli b/user-contrib/Ltac2/tac2match.mli
index 9dba98de63..32ae18a79e 100644
--- a/user-contrib/Ltac2/tac2match.mli
+++ b/user-contrib/Ltac2/tac2match.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index 1ece3d4242..a37fe2f7a5 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2print.mli b/user-contrib/Ltac2/tac2print.mli
index 4c9fcb4016..df5b03f82a 100644
--- a/user-contrib/Ltac2/tac2print.mli
+++ b/user-contrib/Ltac2/tac2print.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2qexpr.mli b/user-contrib/Ltac2/tac2qexpr.mli
index 736c0a96ac..d02df77d06 100644
--- a/user-contrib/Ltac2/tac2qexpr.mli
+++ b/user-contrib/Ltac2/tac2qexpr.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index 26ffe000ad..a2d7013dfa 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index f1564cd443..f9c41b57dc 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index ce510dad16..895b6d3975 100644
--- a/user-contrib/Ltac2/tac2stdlib.ml
+++ b/user-contrib/Ltac2/tac2stdlib.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2stdlib.mli b/user-contrib/Ltac2/tac2stdlib.mli
index 6008a066ec..dca0788f37 100644
--- a/user-contrib/Ltac2/tac2stdlib.mli
+++ b/user-contrib/Ltac2/tac2stdlib.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 8a14be9ca7..30ee1a0b4c 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli
index 1f8f8d5240..f63f7e722a 100644
--- a/user-contrib/Ltac2/tac2tactics.mli
+++ b/user-contrib/Ltac2/tac2tactics.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/user-contrib/Ltac2/tac2types.mli b/user-contrib/Ltac2/tac2types.mli
index 6d98f3f6ef..aaf31e5b42 100644
--- a/user-contrib/Ltac2/tac2types.mli
+++ b/user-contrib/Ltac2/tac2types.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)