summaryrefslogtreecommitdiff
path: root/theories/Classes
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/EquivDec.v4
-rw-r--r--theories/Classes/Equivalence.v4
-rw-r--r--theories/Classes/Init.v4
-rw-r--r--theories/Classes/Morphisms.v4
-rw-r--r--theories/Classes/Morphisms_Prop.v2
-rw-r--r--theories/Classes/Morphisms_Relations.v2
-rw-r--r--theories/Classes/RelationClasses.v4
-rw-r--r--theories/Classes/SetoidClass.v4
-rw-r--r--theories/Classes/SetoidDec.v4
-rw-r--r--theories/Classes/SetoidTactics.v4
10 files changed, 18 insertions, 18 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index cc6e8936..ea1543e3 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.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 *)
@@ -12,7 +12,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: EquivDec.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: EquivDec.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(** Export notations. *)
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 3d8c3434..e562328d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.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 *)
@@ -12,7 +12,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: Equivalence.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Equivalence.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 8cc1216b..eea16129 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.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 *)
@@ -13,7 +13,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: Init.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Init.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(** Hints for the proof search: these combinators should be considered rigid. *)
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index d31829e1..ea869a66 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* 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 *)
@@ -13,7 +13,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: Morphisms.v 13359 2010-07-30 08:46:55Z herbelin $ *)
+(* $Id: Morphisms.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index d4ce9aaa..5a2482d4 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.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/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index e962faf0..a8009f9e 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.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/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 2bfebfd8..94c51bf1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* 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 *)
@@ -15,7 +15,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: RelationClasses.v 13476 2010-09-30 11:42:11Z letouzey $ *)
+(* $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export Coq.Classes.Init.
Require Import Coq.Program.Basics.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index b20f9d88..e9da6874 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.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 *)
@@ -12,7 +12,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: SetoidClass.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: SetoidClass.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Set Implicit Arguments.
Unset Strict Implicit.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index fe775abb..4f70b244 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* 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 *)
@@ -13,7 +13,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: SetoidDec.v 13359 2010-07-30 08:46:55Z herbelin $ *)
+(* $Id: SetoidDec.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Set Implicit Arguments.
Unset Strict Implicit.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 0d43de5a..a1a0c969 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.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 *)
@@ -12,7 +12,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
-(* $Id: SetoidTactics.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: SetoidTactics.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:26:56 +0000