diff options
Diffstat (limited to 'test-suite/bugs/closed/3446.v')
| -rw-r--r-- | test-suite/bugs/closed/3446.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v index dce73e1a..8a0c98c3 100644 --- a/test-suite/bugs/closed/3446.v +++ b/test-suite/bugs/closed/3446.v @@ -48,4 +48,4 @@ Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100. Admitted. Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v := - path_sigma_uncurried P u v o pr1^-1.
\ No newline at end of file + path_sigma_uncurried P u v o pr1^-1. |