aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.mli')
-rw-r--r--printing/printer.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli
index 0855f2d109..f397b2b643 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -192,6 +192,7 @@ type axiom =
| Constant of Constant.t (* An axiom or a constant. *)
| Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
| Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+ | TypeInType of Constant.t (* a constant which relies on type in type *)
type context_object =
| Variable of Id.t (* A section variable or a Let definition *)