Dan Christensen jdchristensen
jdchristensen
/ quotient.patch
Created
August 9, 2021 00:42
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a/theories/Classes/implementations/field_of_fractions.v b/theories/Classes/implementations/field_of_fractions.v | |
| index 853f5f748..015b3e17a 100644 | |
| --- a/theories/Classes/implementations/field_of_fractions.v | |
| +++ b/theories/Classes/implementations/field_of_fractions.v | |
| @@ -301,12 +301,13 @@ Definition F_rec_compute T sT dclass dequiv x | |
| : @F_rec T sT dclass dequiv (' x) = dclass x | |
| := 1. | |
| -Definition F_rec2@{i j} {T:Type@{i} } {sT : IsHSet T} | |
| +Definition F_rec2@{i} {T:Type@{i} } {sT : IsHSet T} |