diff options
Diffstat (limited to 'theories/Classes/Equivalence.v')
| -rw-r--r-- | theories/Classes/Equivalence.v | 5 |
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. |