diff options
| author | Matthieu Sozeau | 2014-10-15 11:41:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 11:49:00 +0200 |
| commit | 707edf9b1e7310bd213678452950aaaa9e4e95f8 (patch) | |
| tree | c35f38ead1b4ab5428b0cf06ecde45405874d77f | |
| parent | 04ee4f9160dec2d854bd45fcff4dac08ada39b61 (diff) | |
Modify the heuristic for unfolding lhs or rhs in evarconv, considering
folded primitive projections in applicative stacks in rhs as named, hence
prefering to unfold the lhs in these cases.
| -rw-r--r-- | pretyping/evarconv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cd55bc26e2..21629553d9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -62,7 +62,7 @@ let eval_flexible_term ts env evd c = | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c | Proj (p, c) -> - if Projection.unfolded p then None + if Projection.unfolded p then assert false else unfold_projection env evd ts p c | _ -> assert false @@ -416,7 +416,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM - else default_fail i) + else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then @@ -611,7 +611,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fst (whd_betaiota_deltazeta_for_iota_state (fst ts) env i Cst_stack.empty (subst1 b c, args))) | Fix _ -> true (* Partially applied fix can be the result of a whd call *) - | Proj (p, c) -> true + | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args | Case _ | App _| Cast _ -> assert false in let rhs_is_stuck_and_unnamed () = let applicative_stack = fst (Stack.strip_app sk2) in |