summaryrefslogtreecommitdiff
path: root/plugins/field
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/field')
-rw-r--r--plugins/field/LegacyField.v2
-rw-r--r--plugins/field/LegacyField_Compl.v2
-rw-r--r--plugins/field/LegacyField_Tactic.v2
-rw-r--r--plugins/field/LegacyField_Theory.v2
-rw-r--r--plugins/field/field.ml42
5 files changed, 5 insertions, 5 deletions
diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v
index efa53b4e..b0e1bc97 100644
--- a/plugins/field/LegacyField.v
+++ b/plugins/field/LegacyField.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
index d4a39296..6d4e49ab 100644
--- a/plugins/field/LegacyField_Compl.v
+++ b/plugins/field/LegacyField_Compl.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
index 5c1f228a..1b04c11a 100644
--- a/plugins/field/LegacyField_Tactic.v
+++ b/plugins/field/LegacyField_Tactic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
index cc8b043f..c7eed29a 100644
--- a/plugins/field/LegacyField_Theory.v
+++ b/plugins/field/LegacyField_Theory.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 238b4c1e..6d3cb25c 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)