summaryrefslogtreecommitdiff
path: root/theories/Classes/Equivalence.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/Equivalence.v')
-rw-r--r--theories/Classes/Equivalence.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5e5895ab..7068bc6b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,15 +12,15 @@
Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
-Require Export Coq.Program.Basics.
+Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Import Coq.Classes.Init.
Require Import Relation_Definitions.
-Require Import Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.