From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
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/indtypes.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 083b0ae40f..8e9b606a58 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -265,13 +265,12 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let univctx =
+  let env' =
     match mie.mind_entry_universes with
-    | Monomorphic_ind_entry ctx -> ctx
-    | Polymorphic_ind_entry ctx -> ctx
-    | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+    | Monomorphic_ind_entry ctx -> push_context_set ctx env
+    | Polymorphic_ind_entry ctx -> push_context ctx env
+    | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
-  let env' = push_context univctx env in
   let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
-- 
cgit v1.2.3