From 3d351474a11ede42b8b48eda51e036eb75ecd5d9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Jun 2014 15:34:01 +0200 Subject: Export the right modules in Setoid, avoiding anomalies in generalized rewriting. --- theories/Classes/CMorphisms.v | 1 - theories/Classes/SetoidTactics.v | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Classes') 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. -- cgit v1.2.3