diff options
| author | Emilio Jesus Gallego Arias | 2018-04-24 18:21:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-01 01:22:00 +0200 |
| commit | fca82378cd2824534383f1f5bc09d08fade1dc17 (patch) | |
| tree | fe95ef8dff5e0e47cb80a54d913fd2a0c8f97ce3 /proofs/proof_bullet.mli | |
| 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 'proofs/proof_bullet.mli')
| -rw-r--r-- | proofs/proof_bullet.mli | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index ffbaa0fac9..a09a7ec1d2 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -14,7 +14,10 @@ (* *) (**********************************************************) -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int (** A [behavior] is the data of a put function which is called when a bullet prefixes a tactic, a suggest function @@ -42,12 +45,8 @@ val register_behavior : behavior -> unit val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - +(** Deprecated *) +val pr_goal_selector : Goal_select.t -> Pp.t +[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] +val get_default_goal_selector : unit -> Goal_select.t +[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] |