From 1071131805c62fb4d9bad6cf65178477cb767872 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 29 Jan 2018 16:57:20 +0100
Subject: proofview: debug API to print a goal

---
 engine/proofview.ml  | 3 +++
 engine/proofview.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 77a884121..766ba7b35 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1067,6 +1067,9 @@ module Goal = struct
   }
 
   let assume (gl : t) = (gl : t)
+
+  let print { sigma; self } = { Evd.it = self; sigma }
+
   let state { state=state } = state
 
   let env {env} = env
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 77f30746d..cab6e3879 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -513,6 +513,7 @@ module Goal : sig
 
   (** Compatibility: avoid if possible *)
   val goal : t -> Evar.t
+  val print : t -> Goal.goal Evd.sigma
 
 end
 
-- 
cgit v1.2.3