diff options
| author | Emilio Jesus Gallego Arias | 2020-04-11 17:19:12 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:43 -0400 |
| commit | e262a6262ebb6c3010cb58e96839b0e3d66e09ac (patch) | |
| tree | 478ded36ca29b20b41119759bbf1a03827c9dfb8 /proofs/proof.mli | |
| parent | 28fc9aff20c39a04ad0e58e1bb8ec52c13631b61 (diff) | |
[proof] Move functions related to `Proof.t` to `Proof`
This makes the API more orthogonal and allows better structure in
future code.
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 0f327e2a25..0e5bdaf07d 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -143,6 +143,8 @@ exception CannotUnfocusThisWay Bullet.push. *) exception NoSuchGoals of int * int +exception NoSuchGoal of Names.Id.t option + (* Unfocusing command. Raises [FullyUnfocused] if the proof is not focused. Raises [CannotUnfocusThisWay] if the proof the unfocusing condition @@ -238,3 +240,10 @@ val refine_by_tactic monad. *) exception SuggestNoSuchGoals of int * t + +(** {6 Helpers to obtain proof state when in an interactive proof } *) +val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env + +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : t -> Evd.evar_map * Environ.env |