From b76827a83f6b7e98bccf484db7f1a3c15add2971 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 8 Apr 2003 14:33:39 +0000
Subject: test: un boolean et une fonction check_for_interrupt inseree dans la
 conversion pour permettre a Coq IDE d'interrompre Coq

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

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a452138fc1..94363b2d19 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -150,6 +150,7 @@ let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = 
+  Util.check_for_interrupt ();
   eqappr cv_pb infos
     (lft1, whd_stack infos term1 [])
     (lft2, whd_stack infos term2 [])
-- 
cgit v1.2.3