From 5b8b02cd060097c3c980b0498257c30eda1ad207 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Dec 2017 20:22:14 +0100
Subject: Fix #6323: stronger restrict universe context vs abstract.

In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.

Universes of a monomorphic reference [c] are considered to appear in
the term [c].
---
 engine/univops.ml | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'engine/univops.ml')

diff --git a/engine/univops.ml b/engine/univops.ml
index 9a9ae12cab..df25d87252 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -9,12 +9,25 @@
 open Univ
 open Constr
 
-let universes_of_constr c =
+let universes_of_constr env c =
+  let open Declarations in
   let rec aux s c = 
     match kind c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) -> 
+    | Const (c, u) ->
+      begin match (Environ.lookup_constant c env).const_universes with
+        | Polymorphic_const _ ->
+          LSet.fold LSet.add (Instance.levels u) s
+        | Monomorphic_const (univs, _) ->
+          LSet.union s univs
+      end
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+      begin match (Environ.lookup_mind mind env).mind_universes with
+        | Cumulative_ind _ | Polymorphic_ind _ ->
+          LSet.fold LSet.add (Instance.levels u) s
+        | Monomorphic_ind (univs,_) ->
+          LSet.union s univs
+      end
+    | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c
-- 
cgit v1.2.3