From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 printing/printer.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.mli')

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 *)
-- 
cgit v1.2.3