diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b4e0459c..372b26aa 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,7 +23,6 @@ open Reductionops open Cbv open Patternops open Locus -open Pretype_errors (* Errors *) @@ -190,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = if Array.for_all (noccurn k) tys && Array.for_all (noccurn (k+nbfix)) bds + && k <= n then (k, List.nth labs (k-1)) else @@ -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 @@ -1212,9 +1205,10 @@ let one_step_reduce env sigma c = (ci,p,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (match reduce_fix (whd_construct_stack env) sigma fix stack with + (try match reduce_fix (whd_construct_stack env) sigma fix stack with | Reduced s' -> s' - | NotReducible -> raise NotStepReducible) + | NotReducible -> raise NotStepReducible + with Redelimination -> raise NotStepReducible) | _ when isEvalRef env x -> let ref,u = destEvalRefU x in (try |