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 | |
| 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')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 2 | ||||
| -rw-r--r-- | toplevel/stm.ml | 2 |
3 files changed, 3 insertions, 3 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) } diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 2adc2feefe..1421aaeed2 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -50,7 +50,7 @@ let adjust_guardness_conditions const = function (* Try all combinations... not optimal *) let env = Global.env() in { const with const_entry_body = - Future.chain ~pure:true const.const_entry_body + Future.chain ~greedy:true ~pure:true const.const_entry_body (fun (body, eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 7ea37b08c7..e632d1dbf6 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -540,7 +540,7 @@ end = struct (* {{{ *) let loc = Option.default Loc.ghost (Loc.get_loc e) in let msg = string_of_ppcmds (print e) in Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); - Stateid.add e ?valid id + Stateid.add (Cerrors.process_vernac_interp_error e) ?valid id let define ?(redefine=false) ?(cache=`No) f id = let str_id = Stateid.to_string id in |