Imported Upstream version 8.3.pl3upstream/8.3.pl3

31 files changed, 290 insertions, 27 deletions

diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
index 3d145d96..490de2a6 100644
--- a/test-suite/bench/lists-100.v
+++ b/test-suite/bench/lists-100.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
index 3d145d96..490de2a6 100644
--- a/test-suite/bench/lists_100.v
+++ b/test-suite/bench/lists_100.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2464.v b/test-suite/bugs/closed/shouldsucceed/2464.v
new file mode 100644
index 00000000..af708587
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2464.v
@@ -0,0 +1,39 @@
+Require Import FSetWeakList.
+Require Import FSetDecide.
+
+Parameter Name : Set.
+Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}.
+
+Module DecidableName.
+Definition t := Name.
+Definition eq := @eq Name.
+Definition eq_refl := @refl_equal Name.
+Definition eq_sym := @sym_eq Name.
+Definition eq_trans := @trans_eq Name.
+Definition eq_dec := eq_Name_dec.
+End DecidableName.
+
+Module NameSetMod := Make(DecidableName).
+
+Module NameSetDec := WDecide (NameSetMod).
+
+Class PartPatchUniverse (pu_type1 pu_type2 : Type)
+                       : Type := mkPartPatchUniverse {
+}.
+Class PatchUniverse {pu_type : Type}
+                    (ppu : PartPatchUniverse pu_type pu_type)
+                  : Type := mkPatchUniverse {
+    pu_nameOf : pu_type -> Name
+}.
+
+Lemma foo : forall (pu_type : Type)
+                   (ppu : PartPatchUniverse pu_type pu_type)
+                   (patchUniverse : PatchUniverse ppu)
+                   (ns ns1 ns2 : NameSetMod.t)
+                   (containsOK : NameSetMod.Equal ns1 ns2)
+                   (p : pu_type)
+                   (HX1 : NameSetMod.Equal ns1 (NameSetMod.add (pu_nameOf p) ns)),
+            NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns).
+Proof.
+NameSetDec.fsetdec.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/shouldsucceed/2467.v
new file mode 100644
index 00000000..ad17814a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2467.v
@@ -0,0 +1,49 @@
+(*
+In the code below, I would expect the
+    NameSetDec.fsetdec.
+to solve the Lemma, but I need to do it in steps instead.
+
+This is a regression relative to FSet,
+
+I have v8.3 (13702).
+*)
+
+Require Import Coq.MSets.MSets.
+
+Parameter Name : Set.
+Parameter Name_compare : Name -> Name -> comparison.
+Parameter Name_compare_sym : forall {x y : Name},
+                             Name_compare y x = CompOpp (Name_compare x y).
+Parameter Name_compare_trans : forall {c : comparison}
+                                      {x y z : Name},
+                               Name_compare x y = c
+                            -> Name_compare y z = c
+                            -> Name_compare x z = c.
+Parameter Name_eq_leibniz : forall {s s' : Name},
+                            Name_compare s s' = Eq
+                         -> s = s'.
+
+Module NameOrderedTypeAlt.
+Definition t := Name.
+Definition compare := Name_compare.
+Definition compare_sym := @Name_compare_sym.
+Definition compare_trans := @Name_compare_trans.
+End NameOrderedTypeAlt.
+
+Module NameOrderedType := OT_from_Alt(NameOrderedTypeAlt).
+
+Module NameOrderedTypeWithLeibniz.
+Include NameOrderedType.
+Definition eq_leibniz := @Name_eq_leibniz.
+End NameOrderedTypeWithLeibniz.
+
+Module NameSetMod := MSetList.MakeWithLeibniz(NameOrderedTypeWithLeibniz).
+Module NameSetDec := WDecide (NameSetMod).
+
+Lemma foo : forall (xs ys : NameSetMod.t)
+                   (n : Name)
+                   (H1 : NameSetMod.Equal xs (NameSetMod.add n ys)),
+            NameSetMod.In n xs.
+Proof.
+NameSetDec.fsetdec.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v
new file mode 100644
index 00000000..a4c95ff9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2608.v
@@ -0,0 +1,34 @@
+
+Module Type T.
+  Parameter Inline t : Type.
+End T.
+
+Module M.
+  Definition t := nat.
+End M.
+
+Module Make (X:T).
+  Include X.
+
+  (* here t is : (Top.Make.t,Top.X.t) *)
+
+  (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t)
+     which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]}
+     which gives : EvalConstRef (Top.Make.t,Top.X.t) *)
+
+End Make.
+
+Module P := Make M.
+
+  (* resolver returned by add_module : Top.P.t=>inline *)
+  (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *)
+
+  (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t)
+     given to subst = {<X#1> |-> Top.M [, Top.M.t=>inline]}
+     which used to give : EvalConstRef (Top.Make.t,Top.M.t)
+     given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]}
+     which used to give : EvalConstRef (Top.P.t,Top.M.t) *)
+
+Definition u := P.t.
+ (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t)
+    and not of (Top.P.t,Top.P.t) *)
diff --git a/test-suite/bugs/closed/shouldsucceed/808_2411.v b/test-suite/bugs/closed/shouldsucceed/808_2411.v
new file mode 100644
index 00000000..1c13e745
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/808_2411.v
@@ -0,0 +1,27 @@
+Section test.
+Variable n:nat.
+Lemma foo: 0 <= n.
+Proof.
+(* declaring an Axiom during a proof makes it immediatly
+   usable, juste as a full Definition. *)
+Axiom bar : n = 1.
+rewrite bar.
+now apply le_S.
+Qed.
+
+Lemma foo' : 0 <= n.
+Proof.
+(* Declaring an Hypothesis during a proof is ok,
+   but this hypothesis won't be usable by the current proof(s),
+   only by later ones. *)
+Hypothesis bar' : n = 1.
+Fail rewrite bar'.
+Abort.
+
+Lemma foo'' : 0 <= n.
+Proof.
+rewrite bar'.
+now apply le_S.
+Qed.
+
+End test.
\ No newline at end of file
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index a08c5154..96e66a0d 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index d000f965..3f8d8784 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index e38fa6e0..e4ef6c95 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 079ad33f..e5915ab1 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index 64537877..ed48c6c2 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index e9fbe969..c02661e0 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index 2b648c13..71d49b58 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index 0ff554d9..ebbd5ca0 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
index 8b36f44b..db52af2f 100644
--- a/test-suite/ideal-features/Apply.v
+++ b/test-suite/ideal-features/Apply.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
index 7d9fb802..da54166a 100644
--- a/test-suite/misc/berardi_test.v
+++ b/test-suite/misc/berardi_test.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
new file mode 100644
index 00000000..23f33081
--- /dev/null
+++ b/test-suite/output/PrintAssumptions.out
@@ -0,0 +1,18 @@
+Axioms:
+foo : nat
+Axioms:
+foo : nat
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
new file mode 100644
index 00000000..f23bc498
--- /dev/null
+++ b/test-suite/output/PrintAssumptions.v
@@ -0,0 +1,96 @@
+
+(** Print Assumption and opaque modules :
+
+  Print Assumption used to consider as axioms the modular fields
+  unexported by their signature, cf bug report #2186. This should
+  now be fixed, let's test this here. *)
+
+(* First, a minimal test-case *)
+
+Axiom foo : nat.
+
+Module Type T.
+ Parameter bar : nat.
+End T.
+
+Module M : T.
+  Module Hide. (* An entire sub-module could be hidden *)
+  Definition x := foo.
+  End Hide.
+  Definition bar := Hide.x.
+End M.
+
+Module N (X:T) : T.
+  Definition y := X.bar. (* A non-exported field *)
+  Definition bar := y.
+End N.
+
+Module P := N M.
+
+Print Assumptions M.bar. (* Should answer: foo *)
+Print Assumptions P.bar. (* Should answer: foo *)
+
+
+(* The original test-case of the bug-report *)
+
+Require Import Arith.
+
+Axiom extensionality : forall P Q (f g:P -> Q),
+  (forall x, f x = g x) -> f = g.
+
+Module Type ADD_COMM_EXT.
+  Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+End ADD_COMM_EXT.
+
+Module AddCommExt_Opaque : ADD_COMM_EXT.
+  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+  Proof.
+    intro n; apply extensionality; auto with arith.
+  Qed.
+End AddCommExt_Opaque.
+
+Module AddCommExt_Transparent <: ADD_COMM_EXT.
+  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+  Proof.
+    intro n; apply extensionality; auto with arith.
+  Qed.
+End AddCommExt_Transparent.
+
+Print Assumptions AddCommExt_Opaque.add_comm_ext.
+(* Should answer: extensionality *)
+
+Print Assumptions AddCommExt_Transparent.add_comm_ext.
+(* Should answer: extensionality *)
+
+Lemma add1_comm_ext_opaque :
+  (fun x => x + 1) = (fun x => 1 + x).
+Proof (AddCommExt_Opaque.add_comm_ext 1).
+
+Lemma add1_comm_ext_transparent :
+  (fun x => x + 1) = (fun x => 1 + x).
+Proof (AddCommExt_Transparent.add_comm_ext 1).
+
+Print Assumptions add1_comm_ext_opaque.
+(* Should answer: extensionality *)
+
+Print Assumptions add1_comm_ext_transparent.
+(* Should answer: extensionality *)
+
+Module Type FALSE_POSITIVE.
+  Axiom add_comm : forall n x, x + n = n + x.
+End FALSE_POSITIVE.
+
+Module false_positive : FALSE_POSITIVE.
+  Lemma add_comm : forall n x, x + n = n + x.
+  Proof. auto with arith. Qed.
+
+  Print Assumptions add_comm.
+  (* Should answer : Closed under the global context *)
+End false_positive.
+
+Lemma comm_plus5 : forall x,
+  x + 5 = 5 + x.
+Proof (false_positive.add_comm 5).
+
+Print Assumptions comm_plus5.
+(* Should answer : Closed under the global context *)
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 47180ef6..d5b94ab4 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index cb90e742..08e8aed2 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Field.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (**** Tests of Field with real numbers ****)
 
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
index 7fd00354..53bcc63a 100644
--- a/test-suite/success/LegacyField.v
+++ b/test-suite/success/LegacyField.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 6322ed2b..324d340a 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Tauto.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Tauto.v 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (**** Tactics Tauto and Intuition ****)
 
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 705bdc45..6cc443bb 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index a94d8b1d..1862ad10 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 5f2d0f39..ff880d00 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 8123726a..4fec6e7f 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index 234c4223..7626ecc4 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index d796cf74..3c8d8ea9 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index fcadd150..41aa3b3e 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 5649e2f7..66c4e080 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
index f75ccfdb..cc40ae07 100644
--- a/test-suite/typeclasses/NewSetoid.v
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)