diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
2 files changed, 5 insertions, 1 deletions
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 |