diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bdd9ed81cf..7c7b31395e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -811,7 +811,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let fold () = let () = if !debug_RAKAM then let open Pp in pp (str "<><><><><>" ++ fnl ()) in - if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l) + (s,cst_l) in match kind_of_term x with | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> @@ -1002,7 +1002,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () in - whrec (Option.default Cst_stack.empty csts) + fun xs -> + let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in + if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res (** reduction machine without global env and refold machinery *) let local_whd_state_gen flags sigma = |