diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-29 00:10:43 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-29 00:19:04 +0200 |
| commit | 6e22ae3f21ae32f298b6e3463448f59a5c7d1f76 (patch) | |
| tree | 1408ca239b7153725c7a77195c6ab3f39ec27d7d /test-suite/bugs/closed/3667.v | |
| parent | 199bb343f7e4367d843ab5ae76ba9a4de89eddbc (diff) | |
In evarconv and unification, expand folded primitive projections to
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
Diffstat (limited to 'test-suite/bugs/closed/3667.v')
| -rw-r--r-- | test-suite/bugs/closed/3667.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3667.v b/test-suite/bugs/closed/3667.v index e0d0e4486..d2fc4d9bf 100644 --- a/test-suite/bugs/closed/3667.v +++ b/test-suite/bugs/closed/3667.v @@ -18,8 +18,8 @@ Definition set_cat : PreCategory. (fun x y => x -> y))). Defined. Goal forall (A : PreCategory) (F : Functor A set_cat) - (a : A) (x : F a), x = x. + (a : A) (x : F a) (nt :NaturalTransformation F F), x = x. intros. - pose (fun c d m => ap10 (commutes x c d m)). + pose (fun c d m => ap10 (commutes nt c d m)). |