aboutsummaryrefslogtreecommitdiff
path: root/theories/setoid_ring
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/setoid_ring
parenta33323d54cf78762f7ba1afc39a2f5a5ddb67a57 (diff)
Update headers in the whole code base.
Add headers to a few files which were missing them.
Diffstat (limited to 'theories/setoid_ring')
-rw-r--r--theories/setoid_ring/Algebra_syntax.v4
-rw-r--r--theories/setoid_ring/ArithRing.v4
-rw-r--r--theories/setoid_ring/BinList.v4
-rw-r--r--theories/setoid_ring/Cring.v4
-rw-r--r--theories/setoid_ring/Field.v4
-rw-r--r--theories/setoid_ring/Field_tac.v4
-rw-r--r--theories/setoid_ring/Field_theory.v4
-rw-r--r--theories/setoid_ring/InitialRing.v4
-rw-r--r--theories/setoid_ring/Integral_domain.v4
-rw-r--r--theories/setoid_ring/NArithRing.v4
-rw-r--r--theories/setoid_ring/Ncring.v4
-rw-r--r--theories/setoid_ring/Ncring_initial.v4
-rw-r--r--theories/setoid_ring/Ncring_polynom.v4
-rw-r--r--theories/setoid_ring/Ncring_tac.v4
-rw-r--r--theories/setoid_ring/RealField.v4
-rw-r--r--theories/setoid_ring/Ring.v4
-rw-r--r--theories/setoid_ring/Ring_base.v4
-rw-r--r--theories/setoid_ring/Ring_polynom.v4
-rw-r--r--theories/setoid_ring/Ring_tac.v4
-rw-r--r--theories/setoid_ring/Ring_theory.v4
-rw-r--r--theories/setoid_ring/Rings_Q.v4
-rw-r--r--theories/setoid_ring/Rings_R.v4
-rw-r--r--theories/setoid_ring/Rings_Z.v4
-rw-r--r--theories/setoid_ring/ZArithRing.v4
24 files changed, 48 insertions, 48 deletions
diff --git a/theories/setoid_ring/Algebra_syntax.v b/theories/setoid_ring/Algebra_syntax.v
index 5f594d29cd..9f6a690283 100644
--- a/theories/setoid_ring/Algebra_syntax.v
+++ b/theories/setoid_ring/Algebra_syntax.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/setoid_ring/ArithRing.v b/theories/setoid_ring/ArithRing.v
index 727e99f0b4..ce56c8dcd9 100644
--- a/theories/setoid_ring/ArithRing.v
+++ b/theories/setoid_ring/ArithRing.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/setoid_ring/BinList.v b/theories/setoid_ring/BinList.v
index 958832274b..b6b8b45e1a 100644
--- a/theories/setoid_ring/BinList.v
+++ b/theories/setoid_ring/BinList.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/setoid_ring/Cring.v b/theories/setoid_ring/Cring.v
index df0313a624..affc078a71 100644
--- a/theories/setoid_ring/Cring.v
+++ b/theories/setoid_ring/Cring.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/setoid_ring/Field.v b/theories/setoid_ring/Field.v
index 9ff07948df..dbc146a524 100644
--- a/theories/setoid_ring/Field.v
+++ b/theories/setoid_ring/Field.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/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v
index a5390efc7f..89a5ca6740 100644
--- a/theories/setoid_ring/Field_tac.v
+++ b/theories/setoid_ring/Field_tac.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/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v
index 3736bc47a5..c12f46bed6 100644
--- a/theories/setoid_ring/Field_theory.v
+++ b/theories/setoid_ring/Field_theory.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/setoid_ring/InitialRing.v b/theories/setoid_ring/InitialRing.v
index dc096554c8..bb98a447dc 100644
--- a/theories/setoid_ring/InitialRing.v
+++ b/theories/setoid_ring/InitialRing.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/setoid_ring/Integral_domain.v b/theories/setoid_ring/Integral_domain.v
index f1394c51d5..87b1068754 100644
--- a/theories/setoid_ring/Integral_domain.v
+++ b/theories/setoid_ring/Integral_domain.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/setoid_ring/NArithRing.v b/theories/setoid_ring/NArithRing.v
index 8cda4ad714..84b5be27c4 100644
--- a/theories/setoid_ring/NArithRing.v
+++ b/theories/setoid_ring/NArithRing.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/setoid_ring/Ncring.v b/theories/setoid_ring/Ncring.v
index 8f3de26272..54c129ad0b 100644
--- a/theories/setoid_ring/Ncring.v
+++ b/theories/setoid_ring/Ncring.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/setoid_ring/Ncring_initial.v b/theories/setoid_ring/Ncring_initial.v
index e40ef6056d..635666593a 100644
--- a/theories/setoid_ring/Ncring_initial.v
+++ b/theories/setoid_ring/Ncring_initial.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/setoid_ring/Ncring_polynom.v b/theories/setoid_ring/Ncring_polynom.v
index 048c8eecf9..8c1267bf00 100644
--- a/theories/setoid_ring/Ncring_polynom.v
+++ b/theories/setoid_ring/Ncring_polynom.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/setoid_ring/Ncring_tac.v b/theories/setoid_ring/Ncring_tac.v
index 65233873b1..59b10fce2c 100644
--- a/theories/setoid_ring/Ncring_tac.v
+++ b/theories/setoid_ring/Ncring_tac.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/setoid_ring/RealField.v b/theories/setoid_ring/RealField.v
index d83fcf3781..16a479bbe6 100644
--- a/theories/setoid_ring/RealField.v
+++ b/theories/setoid_ring/RealField.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/setoid_ring/Ring.v b/theories/setoid_ring/Ring.v
index 35e308565f..a66037a956 100644
--- a/theories/setoid_ring/Ring.v
+++ b/theories/setoid_ring/Ring.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/setoid_ring/Ring_base.v b/theories/setoid_ring/Ring_base.v
index 36e7890fbb..04c7a3a83b 100644
--- a/theories/setoid_ring/Ring_base.v
+++ b/theories/setoid_ring/Ring_base.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/setoid_ring/Ring_polynom.v b/theories/setoid_ring/Ring_polynom.v
index 092114ff0b..e0a3d5a3bf 100644
--- a/theories/setoid_ring/Ring_polynom.v
+++ b/theories/setoid_ring/Ring_polynom.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/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v
index 0a14c0ee5c..df54989169 100644
--- a/theories/setoid_ring/Ring_tac.v
+++ b/theories/setoid_ring/Ring_tac.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/setoid_ring/Ring_theory.v b/theories/setoid_ring/Ring_theory.v
index dc45853458..230e789e21 100644
--- a/theories/setoid_ring/Ring_theory.v
+++ b/theories/setoid_ring/Ring_theory.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/setoid_ring/Rings_Q.v b/theories/setoid_ring/Rings_Q.v
index b3ed0be916..a1343263b7 100644
--- a/theories/setoid_ring/Rings_Q.v
+++ b/theories/setoid_ring/Rings_Q.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/setoid_ring/Rings_R.v b/theories/setoid_ring/Rings_R.v
index ec91fa9e97..22f7a4a392 100644
--- a/theories/setoid_ring/Rings_R.v
+++ b/theories/setoid_ring/Rings_R.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/setoid_ring/Rings_Z.v b/theories/setoid_ring/Rings_Z.v
index 8a51bcea02..f489b00145 100644
--- a/theories/setoid_ring/Rings_Z.v
+++ b/theories/setoid_ring/Rings_Z.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/setoid_ring/ZArithRing.v b/theories/setoid_ring/ZArithRing.v
index 833e19a698..4b4ddba89b 100644
--- a/theories/setoid_ring/ZArithRing.v
+++ b/theories/setoid_ring/ZArithRing.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 *)