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/Setoids | |
| 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/Setoids')
| -rw-r--r-- | theories/Setoids/Setoid.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 34bff6354..983c651ab 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -10,8 +10,7 @@ Set Implicit Arguments. -Require Export Coq.Classes.Equivalence. -Require Export Coq.Relations.Relation_Definitions. +Require Export Coq.Classes.SetoidTactics. (** For backward compatibility *) |