diff options
Diffstat (limited to 'test-suite/bugs/closed/4544.v')
| -rw-r--r-- | test-suite/bugs/closed/4544.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index d14cc86fc..048f31ce3 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -841,7 +841,7 @@ End Truncation_Modalities. Module Import TrM := Modalities_Theory Truncation_Modalities. -Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A). Notation IsSurjection := (IsConnMap -1). |