Remove redundant univ and parameter info from CaseInvert

7 files changed, 17 insertions, 19 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 27b193f144..bed9b639f1 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -489,13 +489,14 @@ let it_destRLambda_or_LetIn_names l c =
               | _ -> DAst.make @@ GApp (c,[a]))
   in aux l [] c
 
-let detype_case computable detype detype_eqns testdep avoid ci p iv c bl =
+let detype_case computable detype detype_eqns testdep avoid ci univs params p iv c bl =
   let synth_type = synthetize_type () in
   let tomatch = detype c in
   let tomatch = match iv with
     | NoInvert -> tomatch
-    | CaseInvert {univs;args} ->
-      let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+    | CaseInvert {indices} ->
+      (* XXX use holes instead of params? *)
+      let t = mkApp (mkIndU (ci.ci_ind,univs), Array.append params indices) in
       DAst.make @@ GCast (tomatch, CastConv (detype t))
   in
   let alias, aliastyp, pred=
@@ -785,7 +786,7 @@ and detype_r d flags avoid env sigma t =
         detype_case comp (detype d flags avoid env sigma)
           (detype_eqns d flags avoid env sigma ci comp)
           (is_nondep_branch sigma) avoid
-          ci p iv c bl
+          ci u pms p iv c bl
     | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef
     | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
     | Int i -> GInt i
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 04feae35d8..d02b015604 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -344,11 +344,7 @@ let get_projections = Environ.get_projections
 
 let make_case_invert env (IndType (((ind,u),params),indices)) ci =
   if Typeops.should_invert_case env ci
-  then
-    let univs = EConstr.EInstance.make u in
-    let params = Array.map_of_list EConstr.of_constr params in
-    let args = Array.append params (Array.of_list indices) in
-    CaseInvert {univs;args}
+  then CaseInvert {indices=Array.of_list indices}
   else NoInvert
 
 let make_case_or_project env sigma indt ci pred c branches =
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 8da615acfc..92e412a537 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -320,13 +320,13 @@ and nf_atom_type env sigma atom =
   | Acase(ans,accu,p,bs) ->
       let a,ta = nf_accu_type env sigma accu in
       let ((mind,_),u as ind),allargs = find_rectype_a env ta in
-      let iv = if Typeops.should_invert_case env ans.asw_ci then
-          CaseInvert {univs=u; args=allargs}
-        else NoInvert
-      in
       let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       let nparams = mib.mind_nparams in
       let params,realargs = Array.chop nparams allargs in
+      let iv = if Typeops.should_invert_case env ans.asw_ci then
+          CaseInvert {indices=realargs}
+        else NoInvert
+      in
       let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT =
         hnf_prod_applist_assum env nparamdecls
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 85214eb245..874457ae52 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -178,7 +178,7 @@ sig
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type 'a case_stk =
-    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+    case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
 
   type 'a member =
   | App of 'a app_node
@@ -234,7 +234,7 @@ struct
 
 
   type 'a case_stk =
-    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+    case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
 
   type 'a member =
   | App of 'a app_node
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e60def72f6..59bc4a8b72 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -58,7 +58,7 @@ module Stack : sig
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type 'a case_stk =
-    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+    case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
 
   type 'a member =
   | App of 'a app_node
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b0ce4fd63a..5b8b367ff2 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -391,8 +391,9 @@ let rec execute env sigma cstr =
         let sigma, lfj = execute_array env sigma lf in
         let sigma = match iv with
           | NoInvert -> sigma
-          | CaseInvert {univs;args} ->
-            let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+          | CaseInvert {indices} ->
+            let args = Array.append pms indices in
+            let t = mkApp (mkIndU (ci.ci_ind,u), args) in
             let sigma, tj = execute env sigma t in
             let sigma, tj = type_judgment env sigma tj in
             let sigma = check_actual_type env sigma cj tj.utj_val in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 314cada2d7..cf6d581066 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -284,7 +284,7 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       let tcase = build_case_type p realargs c in
       let ci = Inductiveops.make_case_info env ind relevance RegularStyle in
       let iv = if Typeops.should_invert_case env ci then
-          CaseInvert {univs=u; args=allargs}
+          CaseInvert {indices=realargs}
         else NoInvert
       in
       nf_stk env sigma (mkCase (Inductive.contract_case env (ci, p, iv, c, branchs))) tcase stk