From 5cac24428e448c12ab292265bb2ffd1146b38c25 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Sep 2020 14:37:43 +0200
Subject: Almost fully moving funind to new proof engine.

---
 proofs/tacmach.ml  | 5 ++++-
 proofs/tacmach.mli | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index ecdbfa5118..1207e0e599 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -99,7 +99,7 @@ let db_pr_goal sigma g =
                    str" "  ++ pc) ++ fnl ()
 
 let pr_gls gls =
-  hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
+  hov 0 (pr_evar_map (Some 2) (pf_env gls) (project gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New = struct
@@ -183,6 +183,9 @@ module New = struct
   let pf_unsafe_type_of gl t =
     pf_apply (unsafe_type_of[@warning "-3"]) gl t
 
+  let pr_gls gl =
+    hov 0 (pr_evar_map (Some 2) (pf_env gl) (project gl) ++ fnl () ++ db_pr_goal (project gl) (Proofview.Goal.goal gl))
+
 end
 
 (* deprecated *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d8f7b7eed8..08f88d46c1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -126,4 +126,5 @@ module New : sig
 
   val pf_nf_evar : Proofview.Goal.t -> constr -> constr
 
+  val pr_gls : Proofview.Goal.t -> Pp.t
 end
-- 
cgit v1.2.3