diff options
| author | Matthieu Sozeau | 2014-09-08 01:48:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-08 01:48:02 +0200 |
| commit | a1a792a0839d12c27164481c14282daf1bc900d3 (patch) | |
| tree | 95c35398c5c72163431a0c47cfdc043f5e64e953 | |
| parent | f5c43cab2e974245ca3bba8d7fc082dffdd5c282 (diff) | |
Fix bug #3589, unification looping due to incorrect use of stack with primitive projections.
| -rw-r--r-- | pretyping/evarconv.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7ce6bc3e2f..99d9364df3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -344,6 +344,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = let default_fail i = (* costly *) UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in + let quick_fail i = (* not costly, loses info *) + UnifFailure (i, NotSameHead) + in let miller_pfenning on_left fallback ev lF tM evd = match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () @@ -399,11 +402,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM else default_fail i) ev lF tM i + and f2 i = + if not (Stack.is_empty skF && Stack.is_empty skM) then + consume_stack on_left apprF apprM i + else quick_fail i and f3 i = - switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) - (whd_betaiota_deltazeta_for_iota_state ts env i cstsM vM) + switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) + (whd_betaiota_deltazeta_for_iota_state ts env i cstsM vM) in - ise_try evd [f1; (consume_stack on_left apprF apprM); f3] in + ise_try evd [f1; f2; f3] in let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = |