From 97614d75a3ae8e515170d1c58c0cbbdf55346558 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Thu, 30 Jan 2014 12:21:05 +0100
Subject: Stack operations of Reductionops in Reductionops.Stack

---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index db6f48547c..3c8ccec6bf 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -186,7 +186,7 @@ let reduction_of_red_expr env =
   | Simpl None -> (simpl,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Cbn f ->
-    (strong (fun env evd x -> zip ~refold:true
+    (strong (fun env evd x -> Stack.zip ~refold:true
       (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)
-- 
cgit v1.2.3