diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 21:38:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 21:38:58 +0200 |
| commit | e681d5809844c2a1514e0fc6b2a334002466db7a (patch) | |
| tree | f41341a8947fdb6a13e415f85cbd4de3f5a83d7c /theories/Classes/CEquivalence.v | |
| parent | 816353f8bee87a8ae1c70263cc3f2dc8ad5358cd (diff) | |
Update and start testing rewrite-in-type code.
Diffstat (limited to 'theories/Classes/CEquivalence.v')
| -rw-r--r-- | theories/Classes/CEquivalence.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index 68a6dcd63..b540feabf 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -17,8 +17,8 @@ Require Import Coq.Program.Tactics. Require Import Coq.Classes.Init. Require Import Relation_Definitions. -Require Export Coq.Classes.RelationClasses. -Require Import Coq.Classes.Morphisms. +Require Export Coq.Classes.CRelationClasses. +Require Import Coq.Classes.CMorphisms. Set Implicit Arguments. Unset Strict Implicit. |