diff options
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index ee8c530fa2..8d2be43cc8 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -17,6 +17,8 @@ Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. +Require Export Coq.Classes.Equivalence. +Require Export Coq.Relations.Relation_Definitions. Set Implicit Arguments. Unset Strict Implicit. @@ -65,6 +67,8 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) Require Import Coq.Program.Tactics. +Open Local Scope signature_scope. + Ltac red_subst_eq_morphism concl := match concl with | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R' |