summaryrefslogtreecommitdiff
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /pretyping/tacred.ml
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml12
1 files changed, 8 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fc35e2d3..6a26027c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -576,7 +576,6 @@ let inSimplBehaviour = declare_object { (default_object "SIMPLBEHAVIOUR") with
let set_simpl_behaviour local r (recargs, nargs, flags as req) =
let nargs = if List.mem `SimplNeverUnfold flags then max_int else nargs in
- let nargs = List.fold_left max nargs recargs in
let behaviour = {
b_nargs = nargs; b_recargs = recargs;
b_dont_expose_case = List.mem `SimplDontExposeCase flags } in
@@ -610,10 +609,11 @@ let dont_expose_case r =
let rec red_elim_const env sigma ref largs =
let nargs = stack_args_size largs in
- let largs, unfold_anyway =
+ let largs, unfold_anyway, unfold_nonelim =
match recargs ref with
- | None -> largs, false
+ | None -> largs, false, false
| Some (_,n) when nargs < n -> raise Redelimination
+ | Some (x::l,_) when nargs <= List.fold_left max x l -> raise Redelimination
| Some (l,n) ->
List.fold_left (fun stack i ->
let arg = stack_nth stack i in
@@ -621,7 +621,8 @@ let rec red_elim_const env sigma ref largs =
match kind_of_term (fst rarg) with
| Construct _ -> stack_assign stack i (app_stack rarg)
| _ -> raise Redelimination)
- largs l, n >= 0 && l = [] && nargs >= n in
+ largs l, n >= 0 && l = [] && nargs >= n,
+ n >= 0 && l <> [] && nargs >= n in
try match reference_eval sigma env ref with
| EliminationCases n when nargs >= n ->
let c = reference_value sigma env ref in
@@ -651,6 +652,9 @@ let rec red_elim_const env sigma ref largs =
(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta sigma c, rest))
+ | NotAnElimination when unfold_nonelim ->
+ let c = reference_value sigma env ref in
+ whd_betaiotazeta sigma (app_stack (c, largs)), empty_stack
| _ -> raise Redelimination
with Redelimination when unfold_anyway ->
let c = reference_value sigma env ref in