Factorize Case cases in subst_univs_level_constr (trivial cleanup)

The branches were separate because CaseInvert used to contain the univ instance.
SkySkimmer · Jul 3, 2024 · 986e18a · 986e18a
1 parent 2106e7a
commit 986e18a
Showing 1 changed file with 2 additions and 10 deletions.
diff --git a/kernel/vars.ml b/kernel/vars.ml
@@ -392,20 +392,12 @@ let subst_univs_level_constr subst c =
         else
           (changed := true; mkSort s')
 
-      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
-        if UVars.Instance.is_empty u then Constr.map aux t
-        else
-          let u' = f u in
-          if u' == u then Constr.map aux t
-          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br)))
-
-      | Case (ci, u, pms, p, NoInvert, c, br) ->
+      | Case (ci, u, pms, p, iv, c, br) ->
         if UVars.Instance.is_empty u then Constr.map aux t
         else
           let u' = f u in
           if u' == u then Constr.map aux t
-          else
-            (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
+          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,iv,c,br)))
 
       | Array (u,elems,def,ty) ->
         let u' = f u in