diff options
| author | Enrico Tassi | 2016-06-05 21:21:43 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-06 14:04:33 -0400 |
| commit | 845dd3dd17b880999a956839c0d84d46de9e27b8 (patch) | |
| tree | 10897262434b5bfa6a78bceaac8cab33ca7acd1b /stm | |
| parent | e4d66a03148243f7611f4d7c164e775877184e03 (diff) | |
STM: each proof block can be enabled separately
By default we enable only {} and par: that are detectable in
a complete way.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 0e33bea3b2..1fd8325e86 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1115,9 +1115,15 @@ let prev_node { id } = mk_doc_node id (VCS.visit id) let cur_node id = mk_doc_node id (VCS.visit id) +let is_block_name_enabled name = + match !Flags.async_proofs_tac_error_resilience with + | `None -> false + | `All -> true + | `Only l -> List.mem name l + let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in - if !Flags.async_proofs_tac_error_resilience && + if is_block_name_enabled name && (if Flags.async_proofs_is_master () then !Flags.async_proofs_mode != Flags.APoff else true) then @@ -2031,7 +2037,7 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if not !Flags.async_proofs_tac_error_resilience || + if !Flags.async_proofs_tac_error_resilience = `None || (Flags.async_proofs_is_master () && !Flags.async_proofs_mode = Flags.APoff) then f () |