diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-07 00:54:30 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-07 00:56:23 +0200 |
| commit | f7e7dcb3513329d82b21f224bb5c5acec445752e (patch) | |
| tree | 37c2a87dbfe224a433d86f6d25124683a80a3152 /pretyping/evarconv.ml | |
| parent | ff81b7f1ffa594ab9f6fd174238b04cbbb1cfb71 (diff) | |
In flex-flex cases, the undefinedness of an evar can not be preseved after converting
the stacks. Take care of this by recalling unification.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 31 |
1 files changed, 25 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cef821586..a9c4c8dc6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -420,12 +420,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with - |None, Success i' -> solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,ev1,term2) - |Some (r,[]), Success i' -> solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,ev2,Stack.zip(term1,r)) - |Some ([],r), Success i' -> solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,ev1,Stack.zip(term2,r)) + |None, Success i' -> + (* Evar can be defined in i' *) + let ev1' = whd_evar i' (mkEvar ev1) in + if isEvar ev1' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem true pbty,destEvar ev1',term2) + else + evar_eqappr_x ts env evd pbty + ((ev1', sk1), csts1) ((term2, sk2), csts2) + |Some (r,[]), Success i' -> + let ev2' = whd_evar i' (mkEvar ev2) in + if isEvar ev2' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem false pbty,destEvar ev2',Stack.zip(term1,r)) + else + evar_eqappr_x ts env evd pbty + ((ev2', sk1), csts1) ((term2, sk2), csts2) + + |Some ([],r), Success i' -> + let ev1' = whd_evar i' (mkEvar ev1) in + if isEvar ev1' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem true pbty,destEvar ev1',Stack.zip(term2,r)) + else evar_eqappr_x ts env evd pbty + ((ev1', sk1), csts1) ((term2, sk2), csts2) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) and f2 i = |