diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 15:34:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 15:44:43 +0200 |
| commit | 3d351474a11ede42b8b48eda51e036eb75ecd5d9 (patch) | |
| tree | afd28f3f0b5f54f5c222eca19b3888fdaa90ee4e /theories/Classes | |
| parent | 55e46598fac67157a5b2c820be621d254581b888 (diff) | |
Export the right modules in Setoid, avoiding anomalies in generalized rewriting.
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/CMorphisms.v | 1 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 1 |
2 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index b1c2842f7..d36833c71 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -15,7 +15,6 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. -Require Import Setoid. Require Export Coq.Classes.CRelationClasses. Generalizable Variables A eqA B C D R RA RB RC m f x y. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index fa939e22e..415c036a1 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -12,6 +12,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) +Require Coq.Classes.CRelationClasses Coq.Classes.CMorphisms. Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. |