From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 Dec 2020 13:20:54 +0100
Subject: Remove redundant univ and parameter info from CaseInvert

---
 kernel/cooking.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 930efa5d36..f82b754c59 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -88,13 +88,6 @@ let expmod_constr cache modlist c =
           let u = Instance.append u' u in
           let pms = Array.append prefix pms in
           let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
-          let iv = match iv with
-            | NoInvert -> NoInvert
-            | CaseInvert {univs; args;} ->
-              let univs = Instance.append u' univs in
-              let args = Array.append prefix args in
-              CaseInvert {univs; args;}
-          in
           Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
         | exception Not_found ->
           Constr.map substrec c
-- 
cgit v1.2.3