From a681e57e3c76dff2fe710ce533179ea659d8de0b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Dec 2013 18:20:22 +0100
Subject: STM: capture type checking error (Closes: 3195)

Also, the future chain that reaches the kernel is greedy.
If the user executes step by step, then the error is raised immediately.
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index b2e0e97366..bf226b0bf9 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -69,7 +69,7 @@ let red_constant_entry n ce = function
   | Some red ->
       let proof_out = ce.const_entry_body in
       let env = Global.env () in
-      { ce with const_entry_body = Future.chain ~pure:true proof_out
+      { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
         (fun (body,eff) ->
            under_binders env
              (fst (reduction_of_red_expr env red)) n body,eff) }
-- 
cgit v1.2.3