summaryrefslogtreecommitdiff
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /pretyping/tacred.ml
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml14
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