diff options
| author | Matthieu Sozeau | 2014-08-28 11:58:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-28 19:55:01 +0200 |
| commit | 3fdfb3ccb7986b1e4c7685b440a62730107a639f (patch) | |
| tree | e07a201af28e25a6513527b528d2c8b48b27af9d /pretyping | |
| parent | ee6743d2879d874cad13bd05b5be3847ac27062e (diff) | |
There are some occurs-check cases that can be handled by imitation (using pruning),
hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but
backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 23358bab5e..04c69d74ae 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -319,19 +319,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 = destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta ts env evd term1 in let term2 = apprec_nohdbeta ts env evd term2 in - begin match kind_of_term term1, kind_of_term term2 with - | Evar ev, _ when Evd.is_undefined evd (fst ev) - && noccur_evar env evd (fst ev) term2 -> - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev,term2) - | _, Evar ev when Evd.is_undefined evd (fst ev) - && noccur_evar env evd (fst ev) term1 -> - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev,term1) - | _ -> + let default () = evar_eqappr_x ts env evd pbty (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) + in + begin match kind_of_term term1, kind_of_term term2 with + | Evar ev, _ when Evd.is_undefined evd (fst ev) -> + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem true pbty,ev,term2) with + | UnifFailure (_,OccurCheck _) -> + (* Eta-expansion might apply *) default () + | x -> x) + | _, Evar ev when Evd.is_undefined evd (fst ev) -> + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem false pbty,ev,term1) with + | UnifFailure (_, OccurCheck _) -> + (* Eta-expansion might apply *) default () + | x -> x) + | _ -> default () end and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty |