aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.mli
diff options
context:
space:
mode:
authorSimonBoulier2018-11-05 11:45:47 +0100
committerSimonBoulier2019-08-16 11:43:51 +0200
commit33f7877dc675cd1c2ce5ffd8da04e65b4d029676 (patch)
treea59cd301dd693382aba593825309a7e214ea21f0 /printing/printer.mli
parentbc4560fa6c88aadcb2ee8312a950a7ce17fc33ee (diff)
Add [Print Typing Flags] command.
Diffstat (limited to 'printing/printer.mli')
-rw-r--r--printing/printer.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli
index a72f319636..0855f2d109 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -207,3 +207,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
+
+val pr_typing_flags : Declarations.typing_flags -> Pp.t