From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 18 Sep 2017 14:50:07 +0200
Subject: When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
---
 kernel/univ.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7fe4f8274..64afb95d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,6 +1053,7 @@ struct
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
 
+  let size (univs,_) = LSet.cardinal univs
 end
 
 type universe_context_set = ContextSet.t
-- 
cgit v1.2.3