diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 18:21:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-01 01:22:00 +0200 |
| commit | fca82378cd2824534383f1f5bc09d08fade1dc17 (patch) | |
| tree | fe95ef8dff5e0e47cb80a54d913fd2a0c8f97ce3 /stm/stm.ml | |
| parent | 8f477d20f6c933537d80bd838b04d13042a12011 (diff) | |
[api] Move bullets and goals selectors to `proofs/`
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index cbd324f5c..9ea6a305e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2288,7 +2288,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; - fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); + fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. |