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 | |
| 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')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 4 |
2 files changed, 3 insertions, 3 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 diff --git a/stm/stm.ml b/stm/stm.ml index 28d5447c44..f3ae32a719 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -881,7 +881,7 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy type proof_part = - Lemmas.Stack.t option * + Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) @@ -1168,7 +1168,7 @@ end = struct (* {{{ *) let get_proof ~doc id = match state_of_id ~doc id with - | `Valid (Some vstate) -> Option.map (Lemmas.Stack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas + | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas | _ -> None let undo_vernac_classifier v ~doc = |