diff options
| -rw-r--r-- | pretyping/evarconv.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 67d650b112..f1845af7f2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -788,7 +788,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else UnifFailure (i,NotSameHead) and f3 i = miller true (sp1,al1) appr1 appr2 i and f4 i = miller false (sp2,al2) appr2 appr1 i - and f5 i = consume true appr1 appr2 i in + and f5 i = + (** We ensure failure of consuming the stacks does not + propagate an error about unification of the stacks while + the heads themselves cannot be unified, so we return + NotSameHead. *) + match consume true appr1 appr2 i with + | Success _ as x -> x + | UnifFailure _ -> quick_fail i + in ise_try evd [f1; f2; f3; f4; f5] | Flexible ev1, MaybeFlexible v2 -> |