diff options
Diffstat (limited to 'test-suite/bugs/closed/3566.v')
| -rw-r--r-- | test-suite/bugs/closed/3566.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v index e0075b8339..d71727be57 100644 --- a/test-suite/bugs/closed/3566.v +++ b/test-suite/bugs/closed/3566.v @@ -18,4 +18,5 @@ Definition lift {T} : T -> Lift T := fun x => x. Goal forall x y : Type, x = y. intros. - pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''. + pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ + (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''. |