aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-06-26 15:34:01 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-06-26 15:44:43 +0200
commit3d351474a11ede42b8b48eda51e036eb75ecd5d9 (patch)
treeafd28f3f0b5f54f5c222eca19b3888fdaa90ee4e /theories
parent55e46598fac67157a5b2c820be621d254581b888 (diff)
Export the right modules in Setoid, avoiding anomalies in generalized rewriting.
Diffstat (limited to 'theories')
-rw-r--r--theories/Classes/CMorphisms.v1
-rw-r--r--theories/Classes/SetoidTactics.v1
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.