diff options
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 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. |