aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/goal.mli')
-rw-r--r--proofs/goal.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli
index cd71d11f8..6d3ec8bd4 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -20,7 +20,7 @@ val uid : goal -> string
val get_by_uid : string -> goal
(* Debugging help *)
-val pr_goal : goal -> Pp.std_ppcmds
+val pr_goal : goal -> Pp.t
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the