diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-22 11:09:53 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-22 11:09:53 +0000 |
| commit | b2ace76af93190c4f08af614869c4a7a728929cf (patch) | |
| tree | 00801716a3add4902f76009248761412a6e9a9ea /theories/Classes/SetoidTactics.v | |
| parent | eb54828e4e6a953a2694d2f3e3af177c20f1fe31 (diff) | |
Compatibility fixes, backtrack on definitions of reflexive,
symmetric... classes for now, merging Relations with RelationClasses
requires some non-trivial changes on implicits but also some definitions
are different (e.g. antisymmetric in Classes is defined w.r.t an
equivalence relation and not eq). Move back to Reflexive and so on.
reflexivity-like tactics fail in the same way as before if Setoid was
not imported. There is now a scope for morphism signatures, hence "==>",
"++>" and "-->" can be given different interpretations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10708 85f007b7-540e-0410-9357-904b9bb8a0f7
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 ee8c530fa..8d2be43cc 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' |