From a071ac178ee9e6ca0cbae14db24e10775b0af881 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 10 Jul 2014 15:39:01 +0200
Subject: Overlooked to remove a change in kernel/closure that made reducing
 under a primitive projection impossible.

---
 kernel/closure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index b12b6502ac..586661d16f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -942,7 +942,7 @@ let rec knh info m stk =
 	  | Some pb ->
 	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
 			 :: zupdate m stk))
-	else (set_norm m; (m,stk))
+	else (m,stk)
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
-- 
cgit v1.2.3