From 2cfb6ec1511c523657f523627f4cfd6c651c6680 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 24 Jan 2013 18:46:39 +0000
Subject: Reductionops: whd_state_gen can take and answers a cst_stack too

+ cst_stack is kept en a meta/evar is "unfold".

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

(limited to 'proofs')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 91ef038ee5..b57ee21189 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -188,7 +188,7 @@ let rec reduction_of_red_expr = function
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Cbn f ->
     (strong (fun env evd x -> zip ~refold:true
-      (whd_state_gen ~refold:true (make_flag f) env evd (x, []))),DEFAULTcast)
+      (fst (whd_state_gen true (make_flag f) env evd (x, [])))),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
   | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
   | Fold cl -> (fold_commands cl,DEFAULTcast)
-- 
cgit v1.2.3