From 6143ac9f9307b2f6863cca019a66cdcbfd52d7ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Feb 2020 17:10:49 +0100
Subject: Do not hardcode specific handling of Prop levels in template poly.

We also factorize a few checks by returning an option when looking for
a potentially template universe.
---
 kernel/indTyping.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indTyping.mli')

diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 723ba5459e..a625caec83 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -44,4 +44,4 @@ val template_polymorphic_univs :
   Univ.ContextSet.t ->
   Constr.rel_context ->
   Univ.Universe.t ->
-  Univ.Level.t option list * Univ.LSet.t
+  (Univ.LSet.t * Univ.Level.t option list) option
-- 
cgit v1.2.3