diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_3422.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_3422.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_3422.v b/test-suite/bugs/closed/bug_3422.v index 460ae8f110..1305104cdb 100644 --- a/test-suite/bugs/closed/bug_3422.v +++ b/test-suite/bugs/closed/bug_3422.v @@ -175,6 +175,7 @@ Global Instance isisomorphism_compose' `{@IsIsomorphism (C -> D) F F' T} : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation := @isisomorphism_compose (C -> D) _ _ T' _ _ T _. +Arguments isisomorphism_compose' {C D F' F''} T' {F} T {H H0}. Section lemmas. Local Open Scope natural_transformation_scope. |