diff options
| author | gareuselesinge | 2012-03-19 10:06:13 +0000 |
|---|---|---|
| committer | gareuselesinge | 2012-03-19 10:06:13 +0000 |
| commit | e0cece37d1e52dd883738efce8eb65150a6020c9 (patch) | |
| tree | 87985f35bad1592513fce3fcf783c0bd88c841ee | |
| parent | 6a6fc7ec30f0fb48d9cfef379f9cab0fa8fffb39 (diff) | |
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
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |