From 3164fb89c2fc3076261bddf5b364667e55c11976 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 13 Jul 2005 16:22:56 +0000
Subject: backtrack modif de knh...

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

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 9725e779cc..2f83657d06 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -968,7 +968,6 @@ let contract_fix_vect fix =
    constructor, cofix, letin, constant), or a neutral term (product,
    inductive) *)
 let rec knh m stk =
-  if is_val m then (incr prune; (m,stk)) else
   match m.term with
     | FLIFT(k,a) -> knh a (zshift k stk)
     | FCLOS(t,e) -> knht e t (zupdate m stk)
-- 
cgit v1.2.3