diff options
| author | Matthieu Sozeau | 2014-08-25 21:46:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-25 21:55:34 +0200 |
| commit | 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (patch) | |
| tree | f7860f13dc18938953ead65c63923aba117d890b /pretyping/evarconv.ml | |
| parent | 12c803053572194c85e4c7b7f347175c7c335858 (diff) | |
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 39 |
1 files changed, 25 insertions, 14 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 68dfb1a1bd..1a699f4afb 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -319,17 +319,22 @@ 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 + 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) -> - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev,term2) + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem true pbty,ev,term2) with + | UnifFailure (_, Pretype_errors.OccurCheck _) -> default () + | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) -> - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev,term1) - | _ -> - 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) + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem false pbty,ev,term1) with + | UnifFailure (_, Pretype_errors.OccurCheck _) -> default () + | x -> x) + | _ -> default () end and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty @@ -338,13 +343,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let miller_pfenning on_left fallback ev lF apprM evd = let tM = Stack.zip apprM in - match is_unification_pattern_evar env evd ev lF tM with + let cont res = + match res with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = nf_evar evd tM in let t2 = solve_pattern_eqn env l1' t2 in - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem on_left pbty,ev,t2) in + solve_simple_eqn (evar_conv_x ts) env evd + (position_problem on_left pbty,ev,t2) + in + try cont (is_unification_pattern_evar_occur env evd ev lF tM) + with Occur -> UnifFailure (evd,OccurCheck (fst ev,tM)) + in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in @@ -407,9 +417,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ev lF apprR evd in let f2 evd = - if isLambda termR then - eta env evd false skR termR skF termF - else UnifFailure (evd,NotSameHead) + match kind_of_term termR with + | Lambda _ -> eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF + | _ -> UnifFailure (evd,NotSameHead) in ise_try evd [f1;f2] in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) |
