From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 22:16:08 +0100
Subject: Proofview.Goal primitive now return EConstrs.

---
 ltac/tactic_debug.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ltac/tactic_debug.ml')

diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index 5cbddc7f64..be1123d5c9 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -51,6 +51,7 @@ let db_pr_goal gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let penv = print_named_context env in
+  let concl = EConstr.Unsafe.to_constr concl in
   let pc = print_constr_env env concl in
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
-- 
cgit v1.2.3