diff options
| author | Matthieu Sozeau | 2014-05-16 19:25:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-16 19:48:22 +0200 |
| commit | d483b7171dafadbe01520bbb6d0c75aa0d6099a7 (patch) | |
| tree | 83141262795fdce2c4c24b62e89e913cb1952349 /pretyping/evarconv.ml | |
| parent | e321cfd21e28161923b84d943cb15c6d775b0d9e (diff) | |
Fix unification of non-unfoldable primitive projections in evarconv.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6bf621b055..aaf7ff65cc 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] |