From cc66d4a0977db4994000bfc7e45937b3ccff3c93 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Aug 2018 15:19:13 +0200
Subject: Avoid repeat universe declarations for constants with split univs

---
 kernel/term_typing.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 43351737e5..f59e07098b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -256,6 +256,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain body (fun ((body,uctx),side_eff) ->
+          (* don't redeclare universes which are declared for the type *)
+          let uctx = Univ.ContextSet.diff uctx univs in
           let j, uctx = match trust with
           | Pure ->
             let env = push_context_set uctx env in
-- 
cgit v1.2.3


From b5c9a9678b2a189edf092f4b8dbebccd49430154 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Aug 2018 15:20:14 +0200
Subject: Avoid repeat univ declaration in cumulative subtyping check

---
 kernel/indtypes.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d7eb865e0a..14decafcd3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,8 +234,7 @@ let check_subtyping cumi paramsctxt env_ar inds =
     let instance_other = Instance.of_array new_levels in
     let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
     let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env = Environ.push_context uctx env_ar in
-    let env = Environ.push_context uctx_other env in
+    let env = Environ.push_context uctx_other env_ar in
     let subtyp_constraints =
       CumulativityInfo.leq_constraints cumi
         (UContext.instance uctx) instance_other
-- 
cgit v1.2.3


From ec4aa4971f7789eeccec2f38f2bb7ec976f87ede Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Aug 2018 15:21:12 +0200
Subject: Do not catch already declared universes in Environ.add_universes

Include is still causing repeat declarations in add_universes_set
---
 kernel/environ.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e7efa5e2c9..778c9a24dd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -365,8 +365,7 @@ let push_constraints_to_env (_,univs) env =
 
 let add_universes strict ctx g =
   let g = Array.fold_left
-	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+            (fun g v -> UGraph.add_universe v strict g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
@@ -376,6 +375,7 @@ let push_context ?(strict=false) ctx env =
 
 let add_universes_set strict ctx g =
   let g = Univ.LSet.fold
+            (* Be lenient, module typing reintroduces universes and constraints due to includes *)
 	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
-- 
cgit v1.2.3