diff options
| author | Matthieu Sozeau | 2014-10-15 13:31:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 13:34:02 +0200 |
| commit | 6bca54599ab2b8ab928bfc92b8ddfb0aeba4345f (patch) | |
| tree | 9730a7ee84044a8ee5062cc6340cc982b31f7722 /pretyping/evarconv.ml | |
| parent | 5e1713d8fe9032a3f5c783cce288b409b6fdf816 (diff) | |
Reenable FO unification of primitive projections and their eta-expanded
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 21629553d9..799ca25233 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -572,7 +572,29 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] - + + (* Catch the p.c ~= p c' cases *) + | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> + let res = + try Some (destApp (Retyping.expand_projection env evd p c [])) + with Retyping.RetypeError _ -> None + in + (match res with + | Some (f1,args1) -> + evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) + (appr2,csts2) + | None -> UnifFailure (evd,NotSameHead)) + + | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> + let res = + try Some (destApp (Retyping.expand_projection env evd p' c' [])) + with Retyping.RetypeError _ -> None + in + (match res with + | Some (f2,args2) -> + evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2) + | None -> UnifFailure (evd,NotSameHead)) + | _, _ -> let f1 i = (* Gather the universe constraints that would make term1 and term2 equal. |