diff options
| author | Emilio Jesus Gallego Arias | 2017-11-19 03:40:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-19 17:38:19 +0100 |
| commit | dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch) | |
| tree | 228d0aeba91a663b947625fd58cebe5bf4537f08 /stm/proofBlockDelimiter.ml | |
| parent | d7a5f439de0208c4a543a81158107b8ccecb6ced (diff) | |
[plugins] Prepare plugin API for functional handling of state.
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b75e4964..77642946cd 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacentries.proof }) -> + | `Valid (Some { Vernacstate.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in |