From d4b3de96f524887013c0955bd5b90f0311f086e6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 11 Oct 2014 12:11:07 +0200 Subject: Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array. --- 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 5186014e2..b80903dc1 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 (d:=H). +Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). Ltac _decide_ P H := let b := fresh "b" in diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index ca4bf9cdf..3bd9dcd12 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 i} [x] _. +Arguments irreflexivity {A R Irreflexive} [x] _. Hint Resolve irreflexivity : ord. -- cgit v1.2.3