From e901ce83ff5c0a3a95d420f6ae10d07312fad4a4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 26 Oct 2020 11:45:28 +0100
Subject: universes_of_constr: don't ignore CaseInvert universes

Not sure if we can get a bug from this omission.
---
 engine/eConstr.ml | 3 +++
 kernel/vars.ml    | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 36297fe243..5136e153ca 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -563,6 +563,9 @@ let universes_of_constr sigma c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       fold sigma aux s c
+    | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
+      fold sigma aux s c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index f7e28b0cfe..a446fa413c 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -348,5 +348,8 @@ let universes_of_constr c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux s c
+    | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+      let s = LSet.fold LSet.add (Instance.levels univs) s in
+      Constr.fold aux s c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
-- 
cgit v1.2.3