diff options
| author | JPR | 2019-05-23 23:28:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:28:55 +0200 |
| commit | d306f5428db0d034aea55d3f0699c67c1f296cc1 (patch) | |
| tree | 540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /theories/Classes | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/EquivDec.v | 2 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 7f26181108..8abd4a3cbb 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -76,7 +76,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -(** The equiv is burried inside the setoid, but we can recover it by specifying +(** The equiv is buried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index f6b240bf20..28394b984e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -77,7 +77,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). Require Import Coq.Arith.Arith. -(** The equiv is burried inside the setoid, but we can recover +(** The equiv is buried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) Program Instance eq_setoid A : Setoid A | 10 := |