aboutsummaryrefslogtreecommitdiff
path: root/ide/interface.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-09-14 16:40:28 +0200
committerPierre-Marie Pédrot2015-09-20 15:20:32 +0200
commitf4584f8a332c9077844e227c8b86d3cb1daf8b12 (patch)
tree8f09f14d3a3273ccdbd7ec86146b70bce5623278 /ide/interface.mli
parent481d2b681463d2758fec6b2417631491be69f216 (diff)
Adding rich printing primitives.
Diffstat (limited to 'ide/interface.mli')
-rw-r--r--ide/interface.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f6d..9d19f1c3c5 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -12,6 +12,7 @@
type raw = bool
type verbose = bool
+type richpp = Richpp.richpp
(** The type of coqtop goals *)
type goal = {