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

---
 kernel/declarations.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 2f6a870c8a..68bd1cbac9 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -94,6 +94,10 @@ type typing_flags = {
 
   cumulative_sprop : bool;
   (** SProp <= Type *)
+
+  allow_uip: bool;
+  (** Allow definitional UIP (breaks termination) *)
+
 }
 
 (* some contraints are in constant_constraints, some other may be in
-- 
cgit v1.2.3