diff options
Diffstat (limited to 'theories/Classes')
-rw-r--r-- | theories/Classes/EquivDec.v | 4 | ||||
-rw-r--r-- | theories/Classes/Equivalence.v | 4 | ||||
-rw-r--r-- | theories/Classes/Init.v | 4 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 4 | ||||
-rw-r--r-- | theories/Classes/Morphisms_Prop.v | 2 | ||||
-rw-r--r-- | theories/Classes/Morphisms_Relations.v | 2 | ||||
-rw-r--r-- | theories/Classes/RelationClasses.v | 4 | ||||
-rw-r--r-- | theories/Classes/SetoidClass.v | 4 | ||||
-rw-r--r-- | theories/Classes/SetoidDec.v | 4 | ||||
-rw-r--r-- | theories/Classes/SetoidTactics.v | 4 |
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. |