diff options
| author | Enrico Tassi | 2016-05-23 13:46:43 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-06 05:48:44 -0400 |
| commit | 8baf120d5cf5045d188f7d926162643a6e7ebcd0 (patch) | |
| tree | c84ad72f9afc6c70c204626b40a00c6608bfd071 | |
| parent | f6cea698f19766087fa56b16ed8dc8cedf079643 (diff) | |
STM: proof block detection for par:
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
| -rw-r--r-- | ltac/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 22 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 2 |
3 files changed, 25 insertions, 1 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index c8287a2c8d..7c161e5cdc 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -366,7 +366,7 @@ VERNAC tactic_mode EXTEND VernacSolve vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => - [ VtProofStep{ parallel = true; proof_block_detection = None }, + [ VtProofStep{ parallel = true; proof_block_detection = Some "par" }, VtLater ] -> [ vernac_solve SelectAll n t def ] diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 1e37209edd..8c50ad9697 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -125,3 +125,25 @@ let dynamic_curly_brace { dynamic_switch = id } = let () = register_proof_block_delimiter "proof-block" static_curly_brace dynamic_curly_brace + +(* ***************** par: ************************************************* *) + +let static_par { entry_point; prev_node } = + match prev_node entry_point with + | None -> None + | Some { id = pid } -> + Some { stop = entry_point.id; start = pid; + dynamic_switch = pid; carry_on_data = unit_val } + +let dynamic_par { dynamic_switch = id } = + match is_focused_goal_simple id with + | `Simple focused -> + `ValidBlock { + base_state = id; + goals_to_admit = focused; + recovery_command = None; + } + | `Not -> `Leaks + +let () = register_proof_block_delimiter "par" static_par dynamic_par + diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index 8455c18485..a55032a470 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -9,6 +9,7 @@ (* This file implements proof block detection for: - blocks delimited by { and } - bullets with indentation + - par: terminator It exports utility functions to ease the development of other proof block detection code. @@ -37,3 +38,4 @@ val unit_val : Stm.DynBlockData.t (* Bullets *) val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet + |