Remove redundant univ and parameter info from CaseInvert

21 files changed, 103 insertions, 134 deletions

diff --git a/checker/values.ml b/checker/values.ml
index b94173429d..907f9f7e32 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -160,7 +160,7 @@ and v_prec = Tuple ("prec_declaration",
                     [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|])
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
-and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|])
+and v_case_invert = Sum ("case_inversion", 1, [|[|Array v_constr|]|])
 
 and v_case_branch = Tuple ("case_branch", [|Array (v_binder_annot v_name); v_constr|])
 
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
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5613bf645e..a32c8f1cd1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -357,7 +357,7 @@ and fterm =
   | FCLOS of constr * fconstr subs
   | FLOCKED
 
-and finvert = Univ.Instance.t * fconstr array
+and finvert = fconstr array
 
 let fterm_of v = v.term
 let set_ntrl v = v.mark <- Mark.set_ntrl v.mark
@@ -582,8 +582,8 @@ let rec to_constr lfts v =
     | FConstruct op -> mkConstructU op
     | FCaseT (ci, u, pms, p, c, ve, env) ->
       to_constr_case lfts ci u pms p NoInvert c ve env
-    | FCaseInvert (ci, u, pms, p, (univs, args), c, ve, env) ->
-      let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in
+    | FCaseInvert (ci, u, pms, p, indices, c, ve, env) ->
+      let iv = CaseInvert {indices=Array.map (to_constr lfts) indices} in
       to_constr_case lfts ci u pms p iv c ve env
     | FFix ((op,(lna,tys,bds)) as fx, e) ->
       if is_subs_id e && is_lift_id lfts then
@@ -1370,8 +1370,8 @@ and knht info e t stk =
         knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,u,pms,p,NoInvert,t,br) ->
         knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk)
-    | Case(ci,u,pms,p,CaseInvert{univs;args},t,br) ->
-      let term = FCaseInvert (ci, u, pms, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
+    | Case(ci,u,pms,p,CaseInvert{indices},t,br) ->
+      let term = FCaseInvert (ci, u, pms, p, (Array.map (mk_clos e) indices), mk_clos e t, br, e) in
       { mark = mark Red Unknown; term }, stk
     | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
     | Cast(a,_,_) -> knht info e a stk
@@ -1478,8 +1478,9 @@ let rec knr info tab m stk =
            kni info tab a (Zprimitive(op,c,rargs,nargs)::s)
              end
      | (_, _, s) -> (m, s))
-  | FCaseInvert (ci, _u, _pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
-    begin match case_inversion info tab ci iv v with
+  | FCaseInvert (ci, u, pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
+    let pms = mk_clos_vect env pms in
+    begin match case_inversion info tab ci u pms iv v with
       | Some c -> knit info tab env c stk
       | None -> (m, stk)
     end
@@ -1496,18 +1497,17 @@ and knit info tab e t stk =
   let (ht,s) = knht info e t stk in
   knr info tab ht s
 
-and case_inversion info tab ci (univs,args) v =
+and case_inversion info tab ci u params indices v =
   let open Declarations in
   (* No binders / lets at all in the unique branch *)
   let v = match v with
   | [| [||], v |] -> v
   | _ -> assert false
   in
-  if Array.is_empty args then Some v
+  if Array.is_empty indices then Some v
   else
     let env = info_env info in
     let ind = ci.ci_ind in
-    let params, indices = Array.chop ci.ci_npar args in
     let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in
     let mib = Environ.lookup_mind (fst ind) env in
     let mip = mib.mind_packets.(snd ind) in
@@ -1516,7 +1516,7 @@ and case_inversion info tab ci (univs,args) v =
     let _ind, expect_args = destApp expect in
     let check_index i index =
       let expected = expect_args.(ci.ci_npar + i) in
-      let expected = Vars.subst_instance_constr univs expected in
+      let expected = Vars.subst_instance_constr u expected in
       let expected = mk_clos psubst expected in
       !conv {info with i_flags=all} tab expected index
     in
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 0dc72025af..30542597c5 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -83,15 +83,15 @@ type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
-type ('constr, 'univs) pcase_invert =
+type 'constr pcase_invert =
   | NoInvert
-  | CaseInvert of { univs : 'univs; args : 'constr array }
+  | CaseInvert of { indices : 'constr array }
 
 type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
 type 'types pcase_return = Name.t Context.binder_annot array * 'types
 
 type ('constr, 'types, 'univs) pcase =
-  case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
 
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
@@ -109,7 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
-  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -125,7 +125,7 @@ type existential = existential_key * constr list
 
 type types = constr
 
-type case_invert = (constr, Instance.t) pcase_invert
+type case_invert = constr pcase_invert
 type case_return = types pcase_return
 type case_branch = constr pcase_branch
 type case = (constr, types, Instance.t) pcase
@@ -481,8 +481,8 @@ let decompose_appvect c =
 
 let fold_invert f acc = function
   | NoInvert -> acc
-  | CaseInvert {univs=_;args} ->
-    Array.fold_left f acc args
+  | CaseInvert {indices} ->
+    Array.fold_left f acc indices
 
 let fold f acc c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -509,8 +509,8 @@ let fold f acc c = match kind c with
 
 let iter_invert f = function
   | NoInvert -> ()
-  | CaseInvert {univs=_; args;} ->
-    Array.iter f args
+  | CaseInvert {indices;} ->
+    Array.iter f indices
 
 let iter f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -624,10 +624,10 @@ let map_return_predicate_with_binders g f l p =
 
 let map_invert f = function
   | NoInvert -> NoInvert
-  | CaseInvert {univs;args;} as orig ->
-    let args' = Array.Smart.map f args in
-    if args == args' then orig
-    else CaseInvert {univs;args=args';}
+  | CaseInvert {indices;} as orig ->
+    let indices' = Array.Smart.map f indices in
+    if indices == indices' then orig
+    else CaseInvert {indices=indices';}
 
 let map f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -695,10 +695,10 @@ let map f c = match kind c with
 
 let fold_map_invert f acc = function
   | NoInvert -> acc, NoInvert
-  | CaseInvert {univs;args;} as orig ->
-    let acc, args' = Array.fold_left_map f acc args in
-    if args==args' then acc, orig
-    else acc, CaseInvert {univs;args=args';}
+  | CaseInvert {indices;} as orig ->
+    let acc, indices' = Array.fold_left_map f acc indices in
+    if indices==indices' then acc, orig
+    else acc, CaseInvert {indices=indices';}
 
 let fold_map_under_context f accu d =
   let (nas, p) = d in
@@ -881,13 +881,12 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let eq_invert eq leq_universes iv1 iv2 =
+let eq_invert eq iv1 iv2 =
   match iv1, iv2 with
   | NoInvert, NoInvert -> true
   | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
-  | CaseInvert {univs;args}, CaseInvert iv2 ->
-    leq_universes univs iv2.univs
-    && Array.equal eq args iv2.args
+  | CaseInvert {indices}, CaseInvert iv2 ->
+    Array.equal eq indices iv2.indices
 
 let eq_under_context eq (_nas1, p1) (_nas2, p2) =
   eq p1 p2
@@ -921,7 +920,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     (** FIXME: what are we doing with u1 = u2 ? *)
     Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 &&
     Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 &&
-    eq_invert (eq 0) (leq_universes None) iv1 iv2 &&
+    eq_invert (eq 0) iv1 iv2 &&
     eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
     Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
@@ -1060,8 +1059,7 @@ let compare_invert f iv1 iv2 =
   | NoInvert, CaseInvert _ -> -1
   | CaseInvert _, NoInvert -> 1
   | CaseInvert iv1, CaseInvert iv2 ->
-    (* univs ignored deliberately *)
-    Array.compare f iv1.args iv2.args
+    Array.compare f iv1.indices iv2.indices
 
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
@@ -1190,9 +1188,8 @@ let invert_eqeq iv1 iv2 =
   match iv1, iv2 with
   | NoInvert, NoInvert -> true
   | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
-  | CaseInvert iv1, CaseInvert iv2 ->
-    iv1.univs == iv2.univs
-    && iv1.args == iv2.args
+  | CaseInvert {indices=i1}, CaseInvert {indices=i2} ->
+    i1 == i2
 
 let hasheq_ctx (nas1, c1) (nas2, c2) =
   array_eqeq nas1 nas2 && c1 == c2
@@ -1368,10 +1365,9 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 
   and sh_invert = function
     | NoInvert -> NoInvert, 0
-    | CaseInvert {univs;args;} ->
-      let univs, hu = sh_instance univs in
-      let args, ha = hash_term_array args in
-      CaseInvert {univs;args;}, combinesmall 1 (combine hu ha)
+    | CaseInvert {indices;} ->
+      let indices, ha = hash_term_array indices in
+      CaseInvert {indices;}, combinesmall 1 ha
 
   and sh_rec t =
     let (y, h) = hash_term t in
@@ -1451,8 +1447,8 @@ let rec hash t =
 
 and hash_invert = function
   | NoInvert -> 0
-  | CaseInvert {univs;args;} ->
-    combinesmall 1 (combine (Instance.hash univs) (hash_term_array args))
+  | CaseInvert {indices;} ->
+    combinesmall 1 (hash_term_array indices)
 
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
@@ -1617,6 +1613,6 @@ let rec debug_print c =
 
 and debug_invert = let open Pp in function
   | NoInvert -> mt()
-  | CaseInvert {univs;args;} ->
-    spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++
-    str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} "
+  | CaseInvert {indices;} ->
+    spc() ++ str"Invert {indices=" ++
+    prlist_with_sep spc debug_print (Array.to_list indices) ++ str "} "
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 17c7da1cf6..57dd850ee7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -49,11 +49,11 @@ type case_info =
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
-type ('constr, 'univs) pcase_invert =
+type 'constr pcase_invert =
   | NoInvert
   (** Normal reduction: match when the scrutinee is a constructor. *)
 
-  | CaseInvert of { univs : 'univs; args : 'constr array; }
+  | CaseInvert of { indices : 'constr array; }
   (** Reduce when the indices match those of the unique constructor.
       (SProp to non SProp only) *)
 
@@ -168,9 +168,9 @@ type 'types pcase_return = Name.t Context.binder_annot array * 'types
 (** Names of the branches *)
 
 type ('constr, 'types, 'univs) pcase =
-  case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
 
-type case_invert = (constr, Univ.Instance.t) pcase_invert
+type case_invert = constr pcase_invert
 type case_return = types pcase_return
 type case_branch = constr pcase_branch
 type case = (constr, types, Univ.Instance.t) pcase
@@ -259,7 +259,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 
   | Ind       of (inductive * 'univs)                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
   | Construct of (constructor * 'univs)              (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
-  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * ('constr,'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -487,7 +487,7 @@ val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -
 
 val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
-val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a
+val fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a
 
 (** [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -495,14 +495,14 @@ val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a
 
 val map : (constr -> constr) -> constr -> constr
 
-val map_invert : ('a -> 'a) -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert
+val map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert
 
 (** Like {!map}, but also has an additional accumulator. *)
 
 val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
 
 val fold_map_invert : ('a -> 'b -> 'a * 'b) ->
-  'a -> ('b, 'c) pcase_invert -> 'a * ('b, 'c) pcase_invert
+  'a -> 'b pcase_invert -> 'a * 'b pcase_invert
 
 (** [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -519,7 +519,7 @@ val map_with_binders :
 
 val iter : (constr -> unit) -> constr -> unit
 
-val iter_invert : ('a -> unit) -> ('a, 'b) pcase_invert -> unit
+val iter_invert : ('a -> unit) -> 'a pcase_invert -> unit
 
 (** [iter_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -597,8 +597,8 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
   constr constr_compare_fn ->
   constr constr_compare_fn
 
-val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool)
-  -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert -> bool
+val eq_invert : ('a -> 'a -> bool)
+  -> 'a pcase_invert -> 'a pcase_invert -> bool
 
 (** {6 Hashconsing} *)
 
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
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 83e41a63ec..741491c917 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -554,12 +554,14 @@ let rec execute env cstr =
         let c', ct = execute env c in
         let iv' = match iv with
           | NoInvert -> NoInvert
-          | CaseInvert {univs;args} ->
-            let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in
+          | CaseInvert {indices} ->
+            let args = Array.append pms indices in
+            let ct' = mkApp (mkIndU (ci.ci_ind,u), args) in
             let (ct', _) : constr * Sorts.t = execute_is_type env ct' in
             let () = conv_leq false env ct ct' in
             let _, args' = decompose_appvect ct' in
-            if args == args' then iv else CaseInvert {univs;args=args'}
+            if args == args' then iv
+            else CaseInvert {indices=Array.sub args' (Array.length pms) (Array.length indices)}
         in
         let p', pt = execute env p in
         let lf', lft = execute_array env lf in
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 0f71057787..b09577d4db 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,13 +253,12 @@ let subst_univs_level_constr subst c =
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
-        if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
         else
           let u' = f u in
-          let univs' = f univs in
-          if u' == u && univs' == univs then Constr.map aux t
-          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)))
+          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) ->
         if Univ.Instance.is_empty u then Constr.map aux t
@@ -314,11 +313,10 @@ let subst_instance_constr subst c =
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
         let u' = f u in
-        let univs' = f univs in
-        if u' == u && univs' == univs then Constr.map aux t
-        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))
+        if u' == u then Constr.map aux t
+        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br))
 
       | Case (ci, u, pms, p, NoInvert, c, br) ->
         if Univ.Instance.is_empty u then Constr.map aux t
@@ -366,11 +364,8 @@ let universes_of_constr c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux s c
-    | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) ->
+    | Case (_, u, _, _, _,_ ,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
-      let s = LSet.fold LSet.add (Instance.levels univs) s in
       Constr.fold aux s c
-    | Case (_, u, _, _, NoInvert, _, _) ->
-      Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
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
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 56bf2b056d..39959d6fb8 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -105,7 +105,7 @@ sig
     | Cst_proj of Projection.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
   | Case of 'a case_stk * Cst_stack.t
@@ -159,7 +159,7 @@ struct
     | Cst_proj of Projection.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
   | Case of 'a case_stk * Cst_stack.t
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 4cc9d99c64..72cac900cd 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -24,7 +24,7 @@ Ltac2 Type case.
 
 Ltac2 Type case_invert := [
 | NoInvert
-| CaseInvert (instance,constr array)
+| CaseInvert (constr array)
 ].
 
 Ltac2 Type kind := [
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 1efbc80e93..64a2b24404 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -109,15 +109,14 @@ let to_rec_declaration (nas, cs) =
 
 let of_case_invert = let open Constr in function
   | NoInvert -> ValInt 0
-  | CaseInvert {univs;args} ->
-    v_blk 0 [|of_instance univs; of_array of_constr args|]
+  | CaseInvert {indices} ->
+    v_blk 0 [|of_array of_constr indices|]
 
 let to_case_invert = let open Constr in function
   | ValInt 0 -> NoInvert
-  | ValBlk (0, [|univs;args|]) ->
-    let univs = to_instance univs in
-    let args = to_array to_constr args in
-    CaseInvert {univs;args}
+  | ValBlk (0, [|indices|]) ->
+    let indices = to_array to_constr indices in
+    CaseInvert {indices}
   | _ -> CErrors.anomaly Pp.(str "unexpected value shape")
 
 let of_result f = function