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

---
 engine/proofview.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 77a884121e..766ba7b35d 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
-- 
cgit v1.2.3


From f7153351bc1d4af2f402671c4937a5186ba77fc3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 14 Feb 2018 09:06:32 +0100
Subject: Proofview: V82.tactic option to not normalize evars

---
 engine/proofview.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 766ba7b35d..0924b7a028 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1202,7 +1202,7 @@ let tclCHECKINTERRUPT =
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
 
-  let tactic tac =
+  let tactic ?(nf_evars=true) tac =
     (* spiwack: we ignore the dependencies between goals here,
        expectingly preserving the semantics of <= 8.2 tactics *)
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -1221,7 +1221,7 @@ module V82 = struct
       let (initgoals_w_state, initevd) =
         Evd.Monad.List.map (fun g_w_s s ->
           let g, w = drop_state g_w_s, get_state g_w_s in
-          let g, s = goal_nf_evar s g in
+          let g, s = if nf_evars then goal_nf_evar s g else g, s in
           goal_with_state g w, s) ps.comb ps.solution
       in
       let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in
-- 
cgit v1.2.3