diff options
| author | Matthieu Sozeau | 2014-08-08 12:44:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-08 12:49:25 +0200 |
| commit | 758f031bc2e2d4a5ece6d515533fafe3e9df98d5 (patch) | |
| tree | c4526eb222f31b410da3bf92ffd4799e0078c707 /pretyping | |
| parent | 21994cc4c617582f4f94577c1c582a7b51b7770b (diff) | |
Fix evarconv not applying eta when it used to. Fixes bug#3319.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ca0644c47e..53b4526c2c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -396,21 +396,21 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; (consume_stack on_left apprF apprM); 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 - match Stack.list_of_app_stack skF with + let f1 evd = + match Stack.list_of_app_stack skF with | None -> consume_stack on_left apprF apprR evd | Some lF -> - let f1 evd = - miller_pfenning on_left - (fun () -> (* Postpone the use of an heuristic *) - switch (fun x y -> - Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR) - ev lF apprR evd - and f2 evd = - if isLambda termR then - eta env evd false skR termR skF termF - else UnifFailure (evd,NotSameHead) - in ise_try evd [f1;f2] in - + miller_pfenning on_left + (fun () -> (* Postpone the use of an heuristic *) + switch (fun x y -> + Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR) + ev lF apprR evd + in + let f2 evd = + if isLambda termR then + eta env evd false skR termR skF termF + else 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 *) let () = if !debug_unification then |