diff options
| author | Emilio Jesus Gallego Arias | 2019-06-09 21:35:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-25 18:25:46 +0200 |
| commit | 9419b85a053f155781db788cfbdfe36308ee0dd1 (patch) | |
| tree | 77fb7e5d062c3bfbc7d27d4517ebf182ada0813c /stm/proofBlockDelimiter.ml | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
[lemmas] Move `Stack` out of Lemmas.
We move the stack of open lemmas from `Lemmas` to `Vernacstate`. The
`Lemmas` module doesn't deal with stacked proofs, so the stack can be
moved to to the proper place; this reduces the size of the API.
Note that `Lemmas` API is still quite imperative, it would be great if
we would return some more information on close proof, for example
about the global environment parts that were modified.
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 4f5cef648b..129444c3b3 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -49,7 +49,7 @@ let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not | `Valid (Some { Vernacstate.lemmas }) -> - Option.cata (Lemmas.Stack.with_top_pstate ~f:(fun proof -> + Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof -> let proof = Proof_global.get_proof proof in let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in |