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

---
 engine/eConstr.ml   |  8 ++------
 engine/eConstr.mli  |  2 +-
 engine/evd.mli      |  4 ++--
 engine/univSubst.ml | 20 +++++---------------
 4 files changed, 10 insertions(+), 24 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7748df1a9b..157995a173 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -37,7 +37,7 @@ type constr = t
 type existential = t pexistential
 type case_return = t pcase_return
 type case_branch = t pcase_branch
-type case_invert = (t, EInstance.t) pcase_invert
+type case_invert = t pcase_invert
 type case = (t, t, EInstance.t) pcase
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
@@ -636,11 +636,7 @@ 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 (_,u,_,_,CaseInvert {univs;args=_},_,_) ->
-      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
-      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
-      fold sigma aux s c
-    | Case (_, u, _, _, NoInvert, _, _) ->
+    | Case (_,u,_,_,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       fold sigma aux s c
     | _ -> fold sigma aux s c
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e914d4f884..0d038e9a67 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -60,7 +60,7 @@ sig
   val is_empty : t -> bool
 end
 
-type case_invert = (t, EInstance.t) pcase_invert
+type case_invert = t pcase_invert
 type case = (t, t, EInstance.t) pcase
 
 type 'a puniverses = 'a * EInstance.t
diff --git a/engine/evd.mli b/engine/evd.mli
index ec9ae6fca9..58f635b7bd 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -772,8 +772,8 @@ module MiniEConstr : sig
     (Constr.t, Constr.types) Context.Named.Declaration.pt
   val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
     (Constr.t, Constr.types) Context.Rel.Declaration.pt
-  val of_case_invert : (constr,Univ.Instance.t) pcase_invert -> (econstr,EInstance.t) pcase_invert
-  val unsafe_to_case_invert : (econstr,EInstance.t) pcase_invert -> (constr,Univ.Instance.t) pcase_invert
+  val of_case_invert : constr pcase_invert -> econstr pcase_invert
+  val unsafe_to_case_invert : econstr pcase_invert -> constr pcase_invert
   val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
     (t, t) Context.Rel.Declaration.pt
   val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index e2721b4822..330ed5d0ad 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -68,15 +68,10 @@ let subst_univs_fn_constr f c =
       let u' = fi u in
         if u' == u then t
         else (changed := true; mkConstructU (c, u'))
-    | Case (ci, u, pms, p, NoInvert, c, br) ->
+    | Case (ci, u, pms, p, iv, c, br) ->
       let u' = fi u in
       if u' == u then map aux t
-      else (changed := true; map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
-    | Case (ci, u, pms, p, CaseInvert{univs;args}, c, br) ->
-      let u' = fi u in
-      let univs' = fi univs in
-      if u' == u && univs' == univs then map aux t
-      else (changed := true; map aux (mkCase (ci, u', pms, p, CaseInvert {univs = univs'; args}, c, br)))
+      else (changed := true; map aux (mkCase (ci, u', pms, p, iv, c, br)))
     | _ -> map aux t
   in
   let c' = aux c in
@@ -156,15 +151,10 @@ let nf_evars_and_universes_opt_subst f subst =
     | Sort (Type u) ->
       let u' = Univ.subst_univs_universe subst u in
       if u' == u then c else mkSort (sort_of_univ u')
-    | Case (ci, u, pms, p, NoInvert, t, br) ->
-      let u' = Instance.subst_fn lsubst u in
-      if u' == u then map aux c
-      else Constr.map aux (mkCase (ci, u', pms, p, NoInvert, t, br))
-    | Case (ci,u,pms,p,CaseInvert {univs;args},t,br) ->
+    | Case (ci,u,pms,p,iv,t,br) ->
       let u' = Instance.subst_fn lsubst u in
-      let univs' = Instance.subst_fn lsubst univs in
-      if u' == u && univs' == univs then Constr.map aux c
-      else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},t,br))
+      if u' == u then Constr.map aux c
+      else Constr.map aux (mkCase (ci,u',pms,p,iv,t,br))
     | Array (u,elems,def,ty) ->
       let u' = Univ.Instance.subst_fn lsubst u in
       let elems' = CArray.Smart.map aux elems in
-- 
cgit v1.2.3