From a99776e10e0b2198d2b811ad82631111fb450f8a Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 12:14:26 +0100
Subject: Update headers in the whole code base.

Add headers to a few files which were missing them.
---
 user-contrib/Ltac2/Array.v         | 4 ++--
 user-contrib/Ltac2/Bool.v          | 4 ++--
 user-contrib/Ltac2/Char.v          | 4 ++--
 user-contrib/Ltac2/Constr.v        | 4 ++--
 user-contrib/Ltac2/Control.v       | 4 ++--
 user-contrib/Ltac2/Env.v           | 4 ++--
 user-contrib/Ltac2/Fresh.v         | 4 ++--
 user-contrib/Ltac2/Ident.v         | 4 ++--
 user-contrib/Ltac2/Init.v          | 4 ++--
 user-contrib/Ltac2/Int.v           | 4 ++--
 user-contrib/Ltac2/List.v          | 4 ++--
 user-contrib/Ltac2/Ltac1.v         | 4 ++--
 user-contrib/Ltac2/Ltac2.v         | 4 ++--
 user-contrib/Ltac2/Message.v       | 4 ++--
 user-contrib/Ltac2/Notations.v     | 4 ++--
 user-contrib/Ltac2/Option.v        | 4 ++--
 user-contrib/Ltac2/Pattern.v       | 4 ++--
 user-contrib/Ltac2/Std.v           | 4 ++--
 user-contrib/Ltac2/String.v        | 4 ++--
 user-contrib/Ltac2/g_ltac2.mlg     | 4 ++--
 user-contrib/Ltac2/tac2core.ml     | 4 ++--
 user-contrib/Ltac2/tac2core.mli    | 4 ++--
 user-contrib/Ltac2/tac2dyn.ml      | 4 ++--
 user-contrib/Ltac2/tac2dyn.mli     | 4 ++--
 user-contrib/Ltac2/tac2entries.ml  | 4 ++--
 user-contrib/Ltac2/tac2entries.mli | 4 ++--
 user-contrib/Ltac2/tac2env.ml      | 4 ++--
 user-contrib/Ltac2/tac2env.mli     | 4 ++--
 user-contrib/Ltac2/tac2expr.mli    | 4 ++--
 user-contrib/Ltac2/tac2extffi.ml   | 4 ++--
 user-contrib/Ltac2/tac2extffi.mli  | 4 ++--
 user-contrib/Ltac2/tac2ffi.ml      | 4 ++--
 user-contrib/Ltac2/tac2ffi.mli     | 4 ++--
 user-contrib/Ltac2/tac2intern.ml   | 4 ++--
 user-contrib/Ltac2/tac2intern.mli  | 4 ++--
 user-contrib/Ltac2/tac2interp.ml   | 4 ++--
 user-contrib/Ltac2/tac2interp.mli  | 4 ++--
 user-contrib/Ltac2/tac2match.ml    | 4 ++--
 user-contrib/Ltac2/tac2match.mli   | 4 ++--
 user-contrib/Ltac2/tac2print.ml    | 4 ++--
 user-contrib/Ltac2/tac2print.mli   | 4 ++--
 user-contrib/Ltac2/tac2qexpr.mli   | 4 ++--
 user-contrib/Ltac2/tac2quote.ml    | 4 ++--
 user-contrib/Ltac2/tac2quote.mli   | 4 ++--
 user-contrib/Ltac2/tac2stdlib.ml   | 4 ++--
 user-contrib/Ltac2/tac2stdlib.mli  | 4 ++--
 user-contrib/Ltac2/tac2tactics.ml  | 4 ++--
 user-contrib/Ltac2/tac2tactics.mli | 4 ++--
 user-contrib/Ltac2/tac2types.mli   | 4 ++--
 49 files changed, 98 insertions(+), 98 deletions(-)

(limited to 'user-contrib')

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          *)
-- 
cgit v1.2.3