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 /pretyping | |
| 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.
Diffstat (limited to 'pretyping')
| -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 |