diff options
| author | Enrico Tassi | 2019-03-04 15:17:34 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-26 14:09:41 +0100 |
| commit | b4561c5047eb2383c2b718fd1cf9da8076497511 (patch) | |
| tree | 086a1b3bcecbd42beb7f5436542be0f470dc60d4 /pretyping | |
| parent | a59d80d3d482813b3c3c1ebce18ae39c3d09e5be (diff) | |
[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 28a97bb91a..0ccc4fd9f9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -503,14 +503,23 @@ let rec evar_conv_x flags env evd pbty term1 term2 = | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem true pbty,ev,term2) with - | UnifFailure (_,OccurCheck _) -> - (* Eta-expansion might apply *) default () + | UnifFailure (_,(OccurCheck _ | NotClean _)) -> + (* Eta-expansion might apply *) + (* OccurCheck: eta-expansion could solve + ?X = {| foo := ?X.(foo) |} + NotClean: pruning in solve_simple_eqn is incomplete wrt + Miller patterns *) + default () | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem false pbty,ev,term1) with - | UnifFailure (_, OccurCheck _) -> - (* Eta-expansion might apply *) default () + | UnifFailure (_, (OccurCheck _ | NotClean _)) -> + (* OccurCheck: eta-expansion could solve + ?X = {| foo := ?X.(foo) |} + NotClean: pruning in solve_simple_eqn is incomplete wrt + Miller patterns *) + default () | x -> x) | _ -> default () end |