diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 17:12:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 17:27:53 +0200 |
| commit | ab53757a3bf57ced503023f3cf9dea5b5503dfea (patch) | |
| tree | 97241209c0348d72fda82fa33d67095f39d32da3 /plugins/ltac/g_ltac.ml4 | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[proof] Move bullets to their own module.
Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.
We thus put the bullet functionality into its own, independent file.
Diffstat (limited to 'plugins/ltac/g_ltac.ml4')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 7855fbcfc..ebeb2d913 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -433,7 +433,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_global.get_default_goal_selector ()) g in + let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => |