diff options
| author | Enrico Tassi | 2019-10-30 10:25:39 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-10-30 10:25:39 +0100 |
| commit | c09f318e200c57750fbefbce00e3f0c4d4ee2c97 (patch) | |
| tree | 6d1198af13ff2658432dcdae63349df9dd63d1d8 /tactics | |
| parent | 99ed41bf8d6d72fc4d5a13d231663bbf48e9ec25 (diff) | |
| parent | 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d (diff) | |
Merge PR #10494: Show diffs in "Show Proof."
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 7 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 4 |
2 files changed, 9 insertions, 2 deletions
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 413c6540a3..47bb0a6af0 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -55,8 +55,7 @@ let get_current_goal_context pf = let env = Global.env () in Evd.from_env env, env -let get_current_context pf = - let p = Proof_global.get_proof pf in +let get_proof_context p = try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -64,6 +63,10 @@ let get_current_context pf = let { Proof.sigma } = Proof.data p in sigma, Global.env () +let get_current_context pf = + let p = Proof_global.get_proof pf in + get_proof_context p + let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 30514191fa..11ce50b659 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : Proof.t -> Evd.evar_map * env + (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. |