diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-16 19:25:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-16 19:48:22 +0200 |
| commit | d483b7171dafadbe01520bbb6d0c75aa0d6099a7 (patch) | |
| tree | 83141262795fdce2c4c24b62e89e913cb1952349 | |
| parent | e321cfd21e28161923b84d943cb15c6d775b0d9e (diff) | |
Fix unification of non-unfoldable primitive projections in evarconv.
| -rw-r--r-- | pretyping/evarconv.ml | 12 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_122.v (renamed from test-suite/bugs/opened/HoTT_coq_122.v) | 2 |
2 files changed, 5 insertions, 9 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6bf621b05..aaf7ff65c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -467,14 +467,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and i [(fun i -> evar_conv_x ts env i CONV c c'); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] - and f2 i = - if is_transparent_constant ts p then - match unfold_projection env p c sk1 with - | Some (c, sk1) -> - let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (c,sk1) in - evar_eqappr_x ts env i pbty out1 (appr2, csts2) - | None -> assert false - else UnifFailure (i, NotSameHead) + and f2 i = + let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2) + in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] diff --git a/test-suite/bugs/opened/HoTT_coq_122.v b/test-suite/bugs/closed/HoTT_coq_122.v index 7e474d0a1..1ba8e5c34 100644 --- a/test-suite/bugs/opened/HoTT_coq_122.v +++ b/test-suite/bugs/closed/HoTT_coq_122.v @@ -22,4 +22,4 @@ Record PreCategory := left_identity : forall a b (f : morphism a b), identity b o f = f }. -Fail Timeout 1 Hint Rewrite @left_identity. (* stack overflow *) +Hint Rewrite @left_identity. (* stack overflow *) |