aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Equivalence.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-16 13:40:45 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-16 13:40:45 +0000
commita76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 (patch)
tree07f989e72b672b508e09f820ab3c32a4016698fe /theories/Classes/Equivalence.v
parentb149e6e21f68d0851f4387dd7182aaca2021041d (diff)
Reorganize Program and Classes theories. Requiring Setoid no longer sets
implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Equivalence.v')
-rw-r--r--theories/Classes/Equivalence.v5
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index a19f8da82..052d21019 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -8,7 +8,6 @@
(************************************************************************)
(* Typeclass-based setoids, tactics and standard instances.
- TODO: explain clrewrite, clsubstitute and so on.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
@@ -17,10 +16,10 @@
(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
Require Export Coq.Program.Basics.
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Tactics.
Require Import Coq.Classes.Init.
-Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.RelationClasses.
Require Export Coq.Classes.Morphisms.
Require Export Coq.Classes.SetoidTactics.