diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-27 13:25:36 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-27 13:25:36 +0100 |
| commit | 525c934044714eb99ca824e5dc929b518aae3730 (patch) | |
| tree | 96d0604f96f50a3be4059eb75cb6f36b86b9317c /test-suite/bugs/closed/3392.v | |
| parent | 321249f0ccc9b7b6fedbab411fac4aa443e0dd43 (diff) | |
Made test for #3392 rely less on unification.
Diffstat (limited to 'test-suite/bugs/closed/3392.v')
| -rw-r--r-- | test-suite/bugs/closed/3392.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v index 29ee14873..02eca64ee 100644 --- a/test-suite/bugs/closed/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -24,9 +24,8 @@ Proof. intros. refine (isequiv_adjointify (functor_forall f g) (functor_forall (f^-1) - (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y - )) _ _); - intros h. + (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f H x # (g (f^-1 x))^-1 y + )) _ _); intros h. - abstract ( apply path_forall; intros b; unfold functor_forall; rewrite eisadj; @@ -37,4 +36,4 @@ Proof. rewrite eissect; apply apD ). -Defined. +Defined.
\ No newline at end of file |