From e0cece37d1e52dd883738efce8eb65150a6020c9 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 19 Mar 2012 10:06:13 +0000
Subject: Fixes bug: #2692 (Arguments/simpl off by 1)

simpl was accessing the reduction stack at position n when
the length of the stack was exactly n.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4e45fb226d..cc1f6f9418 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -577,7 +577,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
@@ -615,6 +614,7 @@ let rec red_elim_const env sigma ref largs =
     match recargs ref with
     | 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
-- 
cgit v1.2.3