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/typeops.mli | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e61d5c399e..65531ed38a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
 (** {6 Type of Cases. } *)
 val judge_of_case : env -> case_info
-  -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-    -> unsafe_judgment
+  -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment
+  -> unsafe_judgment array
+  -> unsafe_judgment
 
 (** {6 Type of global references. } *)
 
@@ -128,3 +129,7 @@ val type_of_prim : env -> CPrimitives.t -> types
 
 val warn_bad_relevance_name : string
 (** Allow the checker to make this warning into an error. *)
+
+val should_invert_case : env -> case_info -> bool
+(** We have case inversion exactly when going from irrelevant nonempty
+   (ie 1 constructor) inductive to relevant type. *)
-- 
cgit v1.2.3