From b2ace76af93190c4f08af614869c4a7a728929cf Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 22 Mar 2008 11:09:53 +0000 Subject: 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 --- theories/Setoids/Setoid.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'theories/Setoids') 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 *) -- cgit v1.2.3