diff options
| author |  Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-09 18:55:28 +0100 |
|---|---|---|
| committer | Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-11 11:44:54 +0100 |
| commit | 1a429d34d1cb1f187dd0cc368cd68cb173f93b82 (patch) | |
| tree | 19fd0f0e164628a2612d7ff8ee76d75b3e800f71 /stm | |
| parent | f36f1d07ee0b9b40d54b9fece942b00e8e5e5d50 (diff) | |
STM: ease re-editing of Admitted proofs
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 092f8eed1..70e242bb5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1010,13 +1010,14 @@ end = struct (* {{{ *) match s, t, r with | `Old c, States _, RespStates l -> List.iter (fun (id,s) -> State.assign id s) l; `End - | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, + | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop }, RespBuiltProof (pl, time) -> feedback (Feedback.InProgress ~-1); t_assign (`Val pl); record_pb_time t_name t_loc time; - if not !Flags.async_proofs_full then `End - else `Stay(t_states,[States t_states]) + if !Flags.async_proofs_full || t_drop + then `Stay(t_states,[States t_states]) + else `End | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> feedback (Feedback.InProgress ~-1); |