From a6d6bca5f024cbdc35924c2cb5e399eb8a2d9c16 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 24 Mar 2016 18:19:08 +0100 Subject: Fix handling of arity of definitional classes. The user-provided sort was ignored for them. --- theories/Classes/CMorphisms.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Classes') diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index c41eb2fa2..10f18fe70 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive Section Normalize. Context (A : Type). - Class Normalizes (m : crelation A) (m' : crelation A) : Prop := + Class Normalizes (m : crelation A) (m' : crelation A) := normalizes : relation_equivalence m m'. (** Current strategy: add [flip] everywhere and reduce using [subrelation] -- cgit v1.2.3