diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d41e0c94f..9a6c2cea2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -949,7 +949,7 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) set_id_for_feedback ?route id; - Aux_file.record_in_aux_set_at ?loc; + Aux_file.record_in_aux_set_at ?loc (); (* We need to check if a command should be filtered from * vernac_entries, as it cannot handle it. This should go away in * future refactorings. @@ -1041,13 +1041,6 @@ end = struct (* {{{ *) | `Stop x -> x | `Cont acc -> next acc - let back_safe () = - let id = - fold_until (fun n (id,_,_,_,_) -> - if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n)) - 0 (VCS.get_branch_pos (VCS.current_branch ())) in - backto id - let undo_vernac_classifier v = try match v with @@ -1212,6 +1205,8 @@ let detect_proof_block id name = (****************************** THE SCHEDULER *********************************) (******************************************************************************) +(* Unused module warning doesn't understand [module rec] *) +[@@@ocaml.warning "-60"] module rec ProofTask : sig type competence = Stateid.t list @@ -1282,7 +1277,6 @@ end = struct (* {{{ *) | RespBuiltProof of Proof_global.closed_proof_output * float | RespError of error | RespStates of (Stateid.t * State.partial_state) list - | RespDone let name = ref "proofworker" let extra_env () = !async_proofs_workers_extra_env @@ -1381,7 +1375,7 @@ end = struct (* {{{ *) if not drop then begin let checked_proof = Future.chain ~pure:false future_proof (fun p -> let pobject, _ = - Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in + Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in stm_vernac_interp stop @@ -2327,6 +2321,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach ~redefine_qed id end (* }}} *) +[@@@ocaml.warning "+60"] (********************************* STM API ************************************) (******************************************************************************) @@ -2433,7 +2428,7 @@ let merge_proof_branch ~valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - VCS.propagate_sideff None; + VCS.propagate_sideff ~replay:None; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = |