Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.

7 files changed, 137 insertions, 85 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c29de27efb..ec255aad03 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -35,6 +35,10 @@ include (Evd.MiniEConstr : module type of Evd.MiniEConstr
 type types = t
 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 = (t, t, EInstance.t) pcase
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -69,7 +73,7 @@ let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
 let mkConstruct c = of_kind (Construct (in_punivs c))
 let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
-let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p))
+let mkCase (ci, u, pms, c, iv, r, p) = of_kind (Case (ci, u, pms, c, iv, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
@@ -195,7 +199,7 @@ let destCoFix sigma c = match kind sigma c with
 | _ -> raise DestKO
 
 let destCase sigma c = match kind sigma c with
-| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p)
+| Case (ci, u, pms, t, iv, c, p) -> (ci, u, pms, t, iv, c, p)
 | _ -> raise DestKO
 
 let destProj sigma c = match kind sigma c with
@@ -320,19 +324,28 @@ let existential_type = Evd.existential_type
 
 let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
 
-let map_under_context f n c =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_under_context f n (unsafe_to_constr c))
-let map_branches f ci br =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
-let map_return_predicate f ci p =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+let of_branches : Constr.case_branch array -> case_branch array =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let unsafe_to_branches : case_branch array -> Constr.case_branch array =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let of_return : Constr.case_return -> case_return =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
 
-let map_user_view sigma f c =
+let unsafe_to_return : case_return -> Constr.case_return =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let map_branches f br =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_branches (Constr.map_branches f (unsafe_to_branches br))
+let map_return_predicate f p =
   let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c)))
+  of_return (Constr.map_return_predicate f (unsafe_to_return p))
 
 let map sigma f c =
   let f c = unsafe_to_constr (f (of_constr c)) in
@@ -346,7 +359,49 @@ let iter sigma f c =
   let f c = f (of_constr c) in
   Constr.iter f (unsafe_to_constr (whd_evar sigma c))
 
-let iter_with_full_binders sigma g f n c =
+let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
+  let u = EInstance.unsafe_to_instance u in
+  let pms = unsafe_to_constr_array pms in
+  let p = unsafe_to_return p in
+  let iv = unsafe_to_case_invert iv in
+  let c = unsafe_to_constr c in
+  let bl = unsafe_to_branches bl in
+  let (ci, p, iv, c, bl) = Inductive.expand_case env (ci, u, pms, p, iv, c, bl) in
+  let p = of_constr p in
+  let c = of_constr c in
+  let iv = of_case_invert iv in
+  let bl = of_constr_array bl in
+  (ci, p, iv, c, bl)
+
+let expand_branch env _sigma u pms (ind, i) (nas, _br) =
+  let open Declarations in
+  let u = EInstance.unsafe_to_instance u in
+  let pms = unsafe_to_constr_array pms in
+  let (mib, mip) = Inductive.lookup_mind_specif env ind in
+  let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in
+  let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in
+  let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+  let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in
+  let ans = Inductive.instantiate_context u subst nas ctx in
+  let ans : rel_context = match Evd.MiniEConstr.unsafe_eq with Refl -> ans in
+  ans
+
+let contract_case env _sigma (ci, p, iv, c, bl) =
+  let p = unsafe_to_constr p in
+  let iv = unsafe_to_case_invert iv in
+  let c = unsafe_to_constr c in
+  let bl = unsafe_to_constr_array bl in
+  let (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, p, iv, c, bl) in
+  let u = EInstance.make u in
+  let pms = of_constr_array pms in
+  let p = of_return p in
+  let iv = of_case_invert iv in
+  let c = of_constr c in
+  let bl = of_branches bl in
+  (ci, u, pms, p, iv, c, bl)
+
+let iter_with_full_binders env sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -357,7 +412,10 @@ let iter_with_full_binders sigma g f n c =
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> List.iter (fun c -> f n c) l
-  | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+  | Case (ci,u,pms,p,iv,c,bl) ->
+    (* FIXME: skip the type annotations *)
+    let (ci, p, iv, c, bl) = expand_case env sigma (ci, u, pms, p, iv, c, bl) in
+    f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
@@ -566,9 +624,13 @@ 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 (_,_,CaseInvert {univs;args=_},_,_) ->
+    | 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, _, _) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
+      fold sigma aux s c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 882dfe2848..2add7b0b5e 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -20,6 +20,8 @@ type t = Evd.econstr
 type types = t
 type constr = t
 type existential = t pexistential
+type case_return = t pcase_return
+type case_branch = t pcase_branch
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -58,6 +60,9 @@ sig
   val is_empty : t -> bool
 end
 
+type case_invert = (t, EInstance.t) pcase_invert
+type case = (t, t, EInstance.t) pcase
+
 type 'a puniverses = 'a * EInstance.t
 
 (** {5 Destructors} *)
@@ -128,7 +133,7 @@ val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
 val mkConstructU : constructor * EInstance.t -> t
 val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
+val mkCase : case -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
@@ -199,7 +204,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
+val destCase : Evd.evar_map -> t -> case
 val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -250,14 +255,12 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 (** {6 Iterators} *)
 
 val map : Evd.evar_map -> (t -> t) -> t -> t
-val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
 val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
-val map_under_context : (t -> t) -> int -> t -> t
-val map_branches : (t -> t) -> case_info -> t array -> t array
-val map_return_predicate : (t -> t) -> case_info -> t -> t
+val map_branches : (t -> t) -> case_branch array -> case_branch array
+val map_return_predicate : (t -> t) -> case_return -> case_return
 val iter : Evd.evar_map -> (t -> unit) -> t -> unit
 val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
-val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
@@ -337,6 +340,17 @@ val fresh_global :
 val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 [@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
+val expand_case : Environ.env -> Evd.evar_map ->
+  case -> (case_info * t * case_invert * t * t array)
+
+val expand_branch : Environ.env -> Evd.evar_map ->
+  EInstance.t -> t array -> constructor -> case_branch -> rel_context
+(** Given a universe instance and parameters for the inductive type,
+    constructs the typed context in which the branch lives. *)
+
+val contract_case : Environ.env -> Evd.evar_map ->
+  (case_info * t * case_invert * t * t array) -> case
+
 (** {5 Extra} *)
 
 val of_existential : Constr.existential -> existential
@@ -345,7 +359,7 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
 
 val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 
-val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+val of_case_invert : Constr.case_invert -> case_invert
 
 (** {5 Unsafe operations} *)
 
@@ -371,7 +385,7 @@ sig
   val to_instance : EInstance.t -> Univ.Instance.t
   (** Physical identity. Does not care for normalization. *)
 
-  val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+  val to_case_invert : case_invert -> Constr.case_invert
 
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ba6a9ea6d9..f9f8268507 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -144,7 +144,7 @@ let head_evar sigma c =
   let c = EConstr.Unsafe.to_constr c in
   let rec hrec c = match kind c with
     | Evar (evk,_)   -> evk
-    | Case (_,_,_,c,_) -> hrec c
+    | Case (_, _, _, _, _, c, _) -> hrec c
     | App (c,_)      -> hrec c
     | Cast (c,_,_)   -> hrec c
     | Proj (p, c)    -> hrec c
diff --git a/engine/evd.mli b/engine/evd.mli
index a6d55c2615..ec9ae6fca9 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) case_invert -> (econstr,EInstance.t) case_invert
-  val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert
+  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_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/termops.ml b/engine/termops.ml
index 66131e1a8f..d331ecc458 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -606,7 +606,7 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right sigma g f l c =
+let map_constr_with_binders_left_to_right env sigma g f l c =
   let open RelDecl in
   let open EConstr in
   match EConstr.kind sigma c with
@@ -650,14 +650,16 @@ let map_constr_with_binders_left_to_right sigma g f l c =
     let al' = List.map_left (f l) al in
       if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
-  | Case (ci,p,iv,b,bl) ->
+  | Case (ci,u,pms,p,iv,b,bl) ->
+      (* FIXME: skip annotations? *)
+      let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, b, bl) in
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let b' = f l b in
       let iv' = map_invert (f l) iv in
       let p' = f l p in
       let bl' = Array.map_left (f l) bl in
       if b' == b && p' == p && iv' == iv && bl' == bl then c
-      else mkCase (ci, p', iv', b', bl')
+      else mkCase (EConstr.contract_case env sigma (ci, p', iv', b', bl'))
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -677,34 +679,8 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       if def' == def && t' == t && ty' == ty then c
       else mkArray(u,t',def',ty')
 
-let rec map_under_context_with_full_binders sigma g f l n d =
-  if n = 0 then f l d else
-    match EConstr.kind sigma d with
-    | LetIn (na,b,t,c) ->
-       let b' = f l b in
-       let t' = f l t in
-       let c' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
-       if b' == b && t' == t && c' == c then d
-       else EConstr.mkLetIn (na,b',t',c')
-    | Lambda (na,t,b) ->
-       let t' = f l t in
-       let b' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
-       if t' == t && b' == b then d
-       else EConstr.mkLambda (na,t',b')
-    | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
-
-let map_branches_with_full_binders sigma g f l ci bl =
-  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
-  let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in
-  if Array.for_all2 (==) bl' bl then bl else bl'
-
-let map_return_predicate_with_full_binders sigma g f l ci p =
-  let n = List.length ci.ci_pp_info.ind_tags in
-  let p' = map_under_context_with_full_binders sigma g f l n p in
-  if p' == p then p else p'
-
 (* strong *)
-let map_constr_with_full_binders_gen userview sigma g f l cstr =
+let map_constr_with_full_binders env sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -736,20 +712,14 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   | Evar (e,al) ->
       let al' = List.map (f l) al in
       if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
-  | Case (ci,p,iv,c,bl) when userview ->
-      let p' = map_return_predicate_with_full_binders sigma g f l ci p in
-      let iv' = map_invert (f l) iv in
-      let c' = f l c in
-      let bl' = map_branches_with_full_binders sigma g f l ci bl in
-      if p==p' && iv'==iv && c==c' && bl'==bl then cstr else
-        mkCase (ci, p', iv', c', bl')
-  | Case (ci,p,iv,c,bl) ->
+  | Case (ci, u, pms, p, iv, c, bl) ->
+      let (ci, p, iv, c, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
       let p' = f l p in
       let iv' = map_invert (f l) iv in
       let c' = f l c in
       let bl' = Array.map (f l) bl in
       if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (ci, p', iv', c', bl')
+        mkCase (EConstr.contract_case env sigma (ci, p', iv', c', bl'))
   | Fix (ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
       let l' = fold_rec_types g fx l in
@@ -770,12 +740,6 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let ty' = f l ty in
       if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty')
 
-let map_constr_with_full_binders sigma g f =
-  map_constr_with_full_binders_gen false sigma g f
-
-let map_constr_with_full_binders_user_view sigma g f =
-  map_constr_with_full_binders_gen true sigma g f
-
 (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
    right according to the usual representation of the constructions as
@@ -783,7 +747,7 @@ let map_constr_with_full_binders_user_view sigma g f =
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_full_binders sigma g f n acc c =
+let fold_constr_with_full_binders env sigma g f n acc c =
   let open EConstr.Vars in
   let open Context.Rel.Declaration in
   match EConstr.kind sigma c with
@@ -795,7 +759,9 @@ let fold_constr_with_full_binders sigma g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Case (ci, u, pms, p, iv, c, bl) ->
+    let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
+    Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
diff --git a/engine/termops.mli b/engine/termops.mli
index 709fa361a9..12df61e4c8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -50,16 +50,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context ->
 (** {6 Generic iterators on constr} *)
 
 val map_constr_with_binders_left_to_right :
-  Evd.evar_map ->
+  Environ.env -> Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
-  Evd.evar_map ->
-  (rel_declaration -> 'a -> 'a) ->
-  ('a -> constr -> constr) -> 'a -> constr -> constr
-val map_constr_with_full_binders_user_view :
-  Evd.evar_map ->
+  Environ.env -> Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
@@ -73,7 +69,7 @@ val map_constr_with_full_binders_user_view :
 val fold_constr_with_binders : Evd.evar_map ->
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
-val fold_constr_with_full_binders : Evd.evar_map ->
+val fold_constr_with_full_binders : Environ.env -> Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> 'b -> constr -> 'b) ->
   'a -> 'b -> constr -> 'b
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 335c2e5e68..e2721b4822 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -68,6 +68,15 @@ 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) ->
+      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)))
     | _ -> map aux t
   in
   let c' = aux c in
@@ -147,10 +156,15 @@ 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,p,CaseInvert {univs;args},t,br) ->
+    | 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) ->
+      let u' = Instance.subst_fn lsubst u in
       let univs' = Instance.subst_fn lsubst univs in
-      if univs' == univs then Constr.map aux c
-      else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
+      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))
     | Array (u,elems,def,ty) ->
       let u' = Univ.Instance.subst_fn lsubst u in
       let elems' = CArray.Smart.map aux elems in