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.
---
 kernel/vars.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel')

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