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 +++
 1 file changed, 3 insertions(+)

(limited to 'engine')

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
 
-- 
cgit v1.2.3