diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2015-02-14 16:10:56 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2015-02-15 17:14:41 +0100 |
| commit | dbb6de3b51dad3c055cb7638fbd6a29df9a6a22d (patch) | |
| tree | f10610ecf62a176b82b5db85853396f6de68316a /pretyping | |
| parent | 8cee2c7ef9e15937fafe60ae43fec7c8bb3678c6 (diff) | |
Fix 'don't expose cases' in cbn
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 9 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 7 |
2 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a23963abc..6059e9ff8 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -842,7 +842,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let (tm',sk'),cst_l' = whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) in - if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk' + let rec is_case x = match kind_of_term x with + | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x + | App (hd, _) -> is_case hd + | Case _ -> true + | _ -> false in + if equal_stacks (x, app_sk) (tm', sk') + || Stack.will_expose_iota sk' + || is_case tm' then fold () else whrec cst_l' (tm', sk' @ sk) else match recargs with diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 91cd08844..372b26aa2 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -597,13 +597,6 @@ let reduce_proj env sigma whfun whfun' c = | _ -> raise Redelimination in redrec c - -let dont_expose_case = function - | EvalVar _ | EvalRel _ | EvalEvar _ -> false - | EvalConst c -> - Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z) - false (ReductionBehaviour.get (ConstRef c)) - let whd_nothing_for_iota env sigma s = let rec whrec (x, stack as s) = match kind_of_term x with |