diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 8805819890..a25cbebe91 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -246,6 +246,7 @@ type axiom = | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) + | UIP of MutInd.t (* An inductive using the special reduction rule. *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) |