diff options
| author | Enrico Tassi | 2013-12-24 18:20:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2013-12-24 18:23:41 +0100 |
| commit | a681e57e3c76dff2fe710ce533179ea659d8de0b (patch) | |
| tree | 6e5a4d2f8aed9dc518fe3d9e6e87bd9600c9a67d /toplevel/command.ml | |
| parent | 18c7a10341b462256b576542412db889d528465f (diff) | |
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.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) } |