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/mod_typing.ml | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8568bf14b8..f7e755f005 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
               environment, because they do not appear in the type of the
               definition. Any inconsistency will be raised at a later stage
               when joining the environment. *)
-	  let env' = Environ.push_context ~strict:true ctx env' in
-	  let c',cst = match cb.const_body with
-	    | Undef _ | OpaqueDef _ ->
-	      let j = Typeops.infer env' c in
-	      let typ = cb.const_type in
-	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-						j.uj_type typ in
-	      j.uj_val, cst'
-	    | Def cs ->
-	       let c' = Mod_subst.force_constr cs in
-	         c, Reduction.infer_conv env' (Environ.universes env') c c'
-	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+          let env' = Environ.push_context ~strict:true ctx env' in
+          let c',cst = match cb.const_body with
+            | Undef _ | OpaqueDef _ ->
+              let j = Typeops.infer env' c in
+              let typ = cb.const_type in
+              let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+                  j.uj_type typ in
+              j.uj_val, cst'
+            | Def cs ->
+              let c' = Mod_subst.force_constr cs in
+              c, Reduction.infer_conv env' (Environ.universes env') c c'
+          in
+          let ctx = Univ.ContextSet.of_context ctx in
+          c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
         | Polymorphic_const uctx ->
           let subst, ctx = Univ.abstract_universes ctx in
           let c = Vars.subst_univs_level_constr subst c in
-- 
cgit v1.2.3