diff options
Diffstat (limited to 'test-suite/bugs/opened/3618.v')
| -rw-r--r-- | test-suite/bugs/opened/3618.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3618.v b/test-suite/bugs/opened/3618.v index cebfcc20ef..bd24c7a7d7 100644 --- a/test-suite/bugs/opened/3618.v +++ b/test-suite/bugs/opened/3618.v @@ -93,7 +93,7 @@ Class inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) := Global Instance hprop_inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) : IsTrunc (trunc_S minus_two) (inO T) . Admitted. -Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} +Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} (P Q : Type) {Q_inO : inO_internal Q} : IsEquiv (fun f => compose f (O_unit P)) := _. |