From d0cd27e209be08ee51a2d609157367f053438a10 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 10 Oct 2014 18:54:56 +0200 Subject: Give the same argument name for the record binder of type class projections and regular records. Easily fixable backwards incompatibility. --- theories/Classes/DecidableClass.v | 2 +- theories/Classes/RelationClasses.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index b80903dc1..5186014e2 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -44,7 +44,7 @@ Qed. (** The generic function that should be used to program, together with some useful tactics. *) -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). +Definition decide P {H : Decidable P} := Decidable_witness (d:=H). Ltac _decide_ P H := let b := fresh "b" in diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 3bd9dcd12..ca4bf9cdf 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -202,7 +202,7 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. -Arguments irreflexivity {A R Irreflexive} [x] _. +Arguments irreflexivity {A R i} [x] _. Hint Resolve irreflexivity : ord. -- cgit v1.2.3