aboutsummaryrefslogtreecommitdiff
path: root/theories/extraction
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 /theories/extraction
parenta33323d54cf78762f7ba1afc39a2f5a5ddb67a57 (diff)
Update headers in the whole code base.
Add headers to a few files which were missing them.
Diffstat (limited to 'theories/extraction')
-rw-r--r--theories/extraction/ExtrOCamlFloats.v4
-rw-r--r--theories/extraction/ExtrOCamlInt63.v4
-rw-r--r--theories/extraction/ExtrOcamlBasic.v4
-rw-r--r--theories/extraction/ExtrOcamlBigIntConv.v4
-rw-r--r--theories/extraction/ExtrOcamlChar.v4
-rw-r--r--theories/extraction/ExtrOcamlIntConv.v4
-rw-r--r--theories/extraction/ExtrOcamlNatBigInt.v4
-rw-r--r--theories/extraction/ExtrOcamlNatInt.v4
-rw-r--r--theories/extraction/ExtrOcamlNativeString.v4
-rw-r--r--theories/extraction/ExtrOcamlString.v4
-rw-r--r--theories/extraction/ExtrOcamlZBigInt.v4
-rw-r--r--theories/extraction/ExtrOcamlZInt.v4
-rw-r--r--theories/extraction/Extraction.v4
13 files changed, 26 insertions, 26 deletions
diff --git a/theories/extraction/ExtrOCamlFloats.v b/theories/extraction/ExtrOCamlFloats.v
index 1891772cc2..02f4b2898b 100644
--- a/theories/extraction/ExtrOCamlFloats.v
+++ b/theories/extraction/ExtrOCamlFloats.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/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v
index a2ee602313..7f7b4af98d 100644
--- a/theories/extraction/ExtrOCamlInt63.v
+++ b/theories/extraction/ExtrOCamlInt63.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/theories/extraction/ExtrOcamlBasic.v b/theories/extraction/ExtrOcamlBasic.v
index 2f82b24862..7730c7b3e0 100644
--- a/theories/extraction/ExtrOcamlBasic.v
+++ b/theories/extraction/ExtrOcamlBasic.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/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v
index f8bc86d087..7740bb41d9 100644
--- a/theories/extraction/ExtrOcamlBigIntConv.v
+++ b/theories/extraction/ExtrOcamlBigIntConv.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/theories/extraction/ExtrOcamlChar.v b/theories/extraction/ExtrOcamlChar.v
index 1e68365dd3..e1ea858fcc 100644
--- a/theories/extraction/ExtrOcamlChar.v
+++ b/theories/extraction/ExtrOcamlChar.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/theories/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v
index 2de1906323..a5be08ece4 100644
--- a/theories/extraction/ExtrOcamlIntConv.v
+++ b/theories/extraction/ExtrOcamlIntConv.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/theories/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v
index a66d6e41fd..8a7ba92a94 100644
--- a/theories/extraction/ExtrOcamlNatBigInt.v
+++ b/theories/extraction/ExtrOcamlNatBigInt.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/theories/extraction/ExtrOcamlNatInt.v b/theories/extraction/ExtrOcamlNatInt.v
index 406a7f0d2b..c662b9d9e6 100644
--- a/theories/extraction/ExtrOcamlNatInt.v
+++ b/theories/extraction/ExtrOcamlNatInt.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/theories/extraction/ExtrOcamlNativeString.v b/theories/extraction/ExtrOcamlNativeString.v
index ec3da1e444..446d41a3ad 100644
--- a/theories/extraction/ExtrOcamlNativeString.v
+++ b/theories/extraction/ExtrOcamlNativeString.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/theories/extraction/ExtrOcamlString.v b/theories/extraction/ExtrOcamlString.v
index 18c5ed3fe4..e47adcf0f0 100644
--- a/theories/extraction/ExtrOcamlString.v
+++ b/theories/extraction/ExtrOcamlString.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/theories/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v
index c36ea50755..40a47b36fa 100644
--- a/theories/extraction/ExtrOcamlZBigInt.v
+++ b/theories/extraction/ExtrOcamlZBigInt.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/theories/extraction/ExtrOcamlZInt.v b/theories/extraction/ExtrOcamlZInt.v
index c7343d2468..8d79604c72 100644
--- a/theories/extraction/ExtrOcamlZInt.v
+++ b/theories/extraction/ExtrOcamlZInt.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/theories/extraction/Extraction.v b/theories/extraction/Extraction.v
index 207c95247e..00b5af74f5 100644
--- a/theories/extraction/Extraction.v
+++ b/theories/extraction/Extraction.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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-07 05:52:24 +0000