diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-11 12:11:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-11 12:15:49 +0200 |
| commit | d4b3de96f524887013c0955bd5b90f0311f086e6 (patch) | |
| tree | ea87e31c9c4681911c9dede29de2d1b51a86deec /theories/Classes | |
| parent | d65496f09c4b68fa318783e53f9cd6d5c18e1eb7 (diff) | |
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.
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/DecidableClass.v | 2 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 2 |
2 files changed, 2 insertions, 2 deletions
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. |