diff options
| author | Jim Fehrle | 2019-07-06 19:25:39 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-10-29 11:25:01 -0700 |
| commit | 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d (patch) | |
| tree | 31fa1c193537525928905d9f22b93b91b4ed1a00 /tactics | |
| parent | f508ddcd2cfff152b8d6291d96e4b87ef9fe2ff9 (diff) | |
Show diffs in "Show Proof."
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
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. |