From 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 6 Jul 2019 19:25:39 -0700
Subject: 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
---
 tactics/pfedit.ml  | 7 +++++--
 tactics/pfedit.mli | 4 ++++
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'tactics')

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.
-- 
cgit v1.2.3