Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

8 files changed, 18 insertions, 9 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 5748a5f3..cc6e8936 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: EquivDec.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (** Export notations. *)
 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 65231ce1..3d8c3434 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: Equivalence.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 6e576c96..8cc1216b 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: Init.v 13323 2010-07-24 15:57:30Z 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 9895c5a4..d31829e1 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: Morphisms.v 13359 2010-07-30 08:46:55Z herbelin $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -23,6 +23,12 @@ Require Export Coq.Classes.RelationClasses.
 Generalizable All Variables.
 Local Obligation Tactic := simpl_relation.
 
+Local Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
+  (at level 200, x binder, y binder, right associativity).
+
+Local Notation "'Π'  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
 (** * Morphisms.
 
    We now turn to the definition of [Proper] and declare standard instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 89c23b3e..1aad3cec 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -15,7 +15,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: RelationClasses.v 13344 2010-07-28 15:04:36Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
@@ -76,7 +76,7 @@ Hint Extern 4 => solve_relation : relations.
 
 Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
-Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
+Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R).
 Proof. tauto. Qed.
 
 Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index ff91bd91..b20f9d88 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: SetoidClass.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 6e92a5de..fe775abb 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -13,13 +13,16 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: SetoidDec.v 13359 2010-07-30 08:46:55Z herbelin $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 Generalizable Variables A B .
 
+Local Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
+  (at level 200, x binder, y binder, right associativity).
+
 (** Export notations. *)
 
 Require Export Coq.Classes.SetoidClass.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index fd3b9f3b..0d43de5a 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -12,7 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
-(* $Id$ *)
+(* $Id: SetoidTactics.v 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.