diff --git a/checker/values.ml b/checker/values.ml
index ebf307958cad..a2b1decdb386 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -128,7 +128,7 @@ let v_boollist = List v_bool
 let v_caseinfo =
   let v_cstyle = v_enum "case_style" 5 in
   let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in
-  v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_relevance;v_cprint|]
+  v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 3
 
@@ -170,7 +170,7 @@ 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|])
 
-and v_case_return = Tuple ("case_return", [|Array (v_binder_annot v_name); v_constr|])
+and v_case_return = Tuple ("case_return", [|Tuple ("case_return'", [|Array (v_binder_annot v_name); v_constr|]); v_relevance|])
 
 let v_rdecl = v_sum "rel_declaration" 0
     [| [|v_binder_annot v_name; v_constr|];               (* LocalAssum *)
diff --git a/dev/ci/user-overlays/18280-SkySkimmer-ci-relevance.sh b/dev/ci/user-overlays/18280-SkySkimmer-ci-relevance.sh
new file mode 100644
index 000000000000..675e887c2c9d
--- /dev/null
+++ b/dev/ci/user-overlays/18280-SkySkimmer-ci-relevance.sh
@@ -0,0 +1,23 @@
+overlay rewriter https://github.com/SkySkimmer/rewriter ci-relevance 18280
+
+overlay coqhammer https://github.com/SkySkimmer/coqhammer ci-relevance 18280
+
+overlay elpi https://github.com/SkySkimmer/coq-elpi ci-relevance 18280
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations ci-relevance 18280
+
+overlay metacoq https://github.com/SkySkimmer/metacoq ci-relevance 18280
+
+overlay unicoq https://github.com/SkySkimmer/unicoq ci-relevance 18280
+
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 ci-relevance 18280
+
+overlay paramcoq https://github.com/SkySkimmer/paramcoq ci-relevance 18280
+
+overlay serapi https://github.com/SkySkimmer/coq-serapi ci-relevance 18280
+
+overlay tactician https://github.com/SkySkimmer/coq-tactician ci-relevance 18280
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof ci-relevance 18280
+
+overlay fiat_crypto https://github.com/SkySkimmer/fiat-crypto ci-relevance 18280
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8e6b048b6880..119d0be3c787 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -348,7 +348,7 @@ let constr_display csr =
       "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
   | Proj (p, r, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
-  | Case (ci,u,pms,(_,p),iv,c,bl) ->
+  | Case (ci,u,pms,((_,p),_),iv,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display (Array.map snd bl))^")"
   | Fix ((t,i),(lna,tl,bl)) ->
@@ -473,7 +473,7 @@ let print_pure_constr csr =
       print_int i; print_string ","; print_int j;
       print_string ","; universes_display u;
       print_string ")"
-  | Case (ci,u,pms,p,iv,c,bl) ->
+  | Case (ci,u,pms,(p,_),iv,c,bl) ->
       let pr_ctx (nas, c) =
         Array.iter (fun na -> print_cut (); name_display na) nas;
         print_string " |- ";
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7169f59eda56..6421eb4bbbc5 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -437,15 +437,15 @@ let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
   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 (ci, (p,r), 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)
+  (ci, (p,r), iv, c, bl)
 
 let annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
-  let (_, p, _, _, bl) = expand_case env sigma case in
+  let (_, (p,r), _, _, bl) = expand_case env sigma case in
   let p =
     (* Too bad we need to fetch this data in the environment, should be in the
       case_info instead. *)
@@ -454,7 +454,7 @@ let annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
   in
   let mk_br c n = decompose_lambda_n_decls sigma n c in
   let bl = Array.map2 mk_br bl ci.ci_cstr_ndecls in
-  (ci, u, pms, p, iv, c, bl)
+  (ci, u, pms, (p,r), iv, c, bl)
 
 let expand_branch env _sigma u pms (ind, i) (nas, _br) =
   let open Declarations in
@@ -469,12 +469,12 @@ let expand_branch env _sigma u pms (ind, i) (nas, _br) =
   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 contract_case env _sigma (ci, (p,r), 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 (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, (p,r), iv, c, bl) in
   let u = EInstance.make u in
   let pms = of_constr_array pms in
   let p = of_return p in
@@ -497,7 +497,7 @@ let iter_with_full_binders env sigma g f n c =
     let l = Evd.expand_existential sigma ev in
     List.iter (fun c -> f n c) l
   | Case (ci,u,pms,p,iv,c,bl) ->
-    let (ci, _, pms, p, iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let (ci, _, pms, (p,_), iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
     let f_ctx (ctx, c) = f (List.fold_right g ctx n) c in
     Array.Fun1.iter f n pms; f_ctx p; iter_invert (f n) iv; f n c; Array.iter f_ctx bl
   | Proj (_,_,c) -> f n c
@@ -731,8 +731,8 @@ let fold_constr_relevance sigma f acc c =
   | Prod (na,_,_) | Lambda (na,_,_) | LetIn (na,_,_,_) ->
     fold_annot_relevance f acc na
 
-  | Case (ci,_u,_params,ret,_iv,_v,brs) ->
-    let acc = f acc ci.ci_relevance in
+  | Case (_,_u,_params,(ret,r),_iv,_v,brs) ->
+    let acc = f acc r in
     let acc = fold_case_under_context_relevance f acc ret in
     let acc = CArray.fold_left (fold_case_under_context_relevance f) acc brs in
     acc
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 568aa43a49bd..1ce564d0dabc 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -428,10 +428,10 @@ val is_global : Environ.env -> 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)
+  case -> (t,t) Inductive.pexpanded_case
 
 val annotate_case : Environ.env -> Evd.evar_map -> case ->
-  case_info * EInstance.t * t array * (rel_context * t) * case_invert * t * (rel_context * t) array
+  case_info * EInstance.t * t array * ((rel_context * t) * Sorts.relevance) * case_invert * t * (rel_context * t) array
 (** Same as above, but doesn't turn contexts into binders *)
 
 val expand_branch : Environ.env -> Evd.evar_map ->
@@ -440,7 +440,7 @@ val expand_branch : Environ.env -> Evd.evar_map ->
     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
+  (t,t) Inductive.pexpanded_case -> case
 
 (** {5 Extra} *)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index f69ed73a883b..78f6751fefa5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -649,8 +649,8 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
   | Evar ev ->
     let ev' = EConstr.map_existential sigma (fun c -> f l c) ev in
     if ev' == ev then c else mkEvar ev'
-  | Case (ci,u,pms,p,iv,b,bl) ->
-      let (ci, _, pms, p0, _, b, bl0) = annotate_case env sigma (ci, u, pms, p, iv, b, bl) in
+  | Case (ci,u,pms,(p,r),iv,b,bl) ->
+      let (ci, _, pms, (p0,_), _, b, bl0) = annotate_case env sigma (ci, u, pms, (p,r), iv, b, bl) in
       let f_ctx (nas, _ as r) (ctx, c) =
         let c' = f (List.fold_right g ctx l) c in
         if c' == c then r else (nas, c')
@@ -662,7 +662,7 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
       let iv' = map_invert (f l) iv in
       let bl' = Array.map_left (fun (c, c0) -> f_ctx c c0) (Array.map2 (fun x y -> (x, y)) bl bl0) in
         if b' == b && pms' == pms && p' == p && iv' == iv && bl' == bl then c
-        else mkCase (ci, u, pms', p', iv', b', bl')
+        else mkCase (ci, u, pms', (p',r), 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
@@ -715,8 +715,8 @@ let map_constr_with_full_binders env sigma g f l cstr =
   | Evar ev ->
     let ev' = EConstr.map_existential sigma (fun c -> f l c) ev in
     if ev' == ev then cstr else mkEvar ev'
-  | Case (ci, u, pms, p, iv, c, bl) ->
-      let (ci, _, pms, p0, _, c, bl0) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+  | Case (ci, u, pms, (p,r), iv, c, bl) ->
+      let (ci, _, pms, (p0,_), _, c, bl0) = annotate_case env sigma (ci, u, pms, (p,r), iv, c, bl) in
       let f_ctx (nas, _ as r) (ctx, c) =
         let c' = f (List.fold_right g ctx l) c in
         if c' == c then r else (nas, c')
@@ -727,7 +727,7 @@ let map_constr_with_full_binders env sigma g f l cstr =
       let c' = f l c in
       let bl' = Array.map2 f_ctx bl bl0 in
       if pms==pms' && p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (ci, u, pms', p', iv', c', bl')
+        mkCase (ci, u, pms', (p',r), 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,7 +770,7 @@ let fold_constr_with_full_binders env sigma g f n acc c =
     let args = Evd.expand_existential sigma ev in
     List.fold_left (fun c -> f n c) acc args
   | Case (ci, u, pms, p, iv, c, bl) ->
-    let (ci, _, pms, p, _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let (ci, _, pms, (p,_), _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
     let f_ctx acc (ctx, c) = f (List.fold_right g ctx n) acc c in
     Array.fold_left f_ctx (f n (fold_invert (f n) (f_ctx (Array.fold_left (f n) acc pms) p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 62b2aa398393..615dd41d52bf 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -190,19 +190,16 @@ let nf_evars_and_universes_opt_subst fevar fqual funiv c =
     | Sort s ->
       let s' = Sorts.subst_fn (fqual, subst_univs_universe funiv) s in
       if s' == s then c else mkSort s'
-    | Case (ci,u,pms,p,iv,t,br) ->
+    | Case (ci,u,pms,(p,rel),iv,t,br) ->
       let u' = Instance.subst_fn flevel u in
-      let ci' =
-        let rel' = frel ci.ci_relevance in
-        if rel' == ci.ci_relevance then ci else { ci with ci_relevance = rel' }
-      in
+      let rel' = frel rel in
       let pms' = Array.Smart.map aux pms in
       let p' = aux_ctx p in
       let iv' = map_invert aux iv in
       let t' = aux t in
       let br' = Array.Smart.map aux_ctx br in
-      if ci' == ci && u' == u && pms' == pms && p' == p && iv' == iv && t' == t && br' == br then c
-      else mkCase (ci', u', pms', p', iv', t', br')
+      if rel' == rel && u' == u && pms' == pms && p' == p && iv' == iv && t' == t && br' == br then c
+      else mkCase (ci, u', pms', (p',rel'), iv', t', br')
     | Array (u,elems,def,ty) ->
       let u' = Instance.subst_fn flevel u in
       let elems' = CArray.Smart.map aux elems in
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 554036240fce..be7c4828a1b2 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -264,11 +264,6 @@ let usubst_binder e x =
   let r' = usubst_relevance e r in
   if r == r' then x else { x with binder_relevance = r' }
 
-let usubst_case_info e ci =
-  let r = ci.ci_relevance in
-  let r' = usubst_relevance e r in
-  if r == r' then ci else { ci with ci_relevance = r' }
-
 let mk_lambda env t =
   let (rvars,t') = Term.decompose_lambda t in
   FLambda(List.length rvars, List.rev rvars, t', env)
@@ -534,11 +529,11 @@ let rec to_constr (lfts, usubst as ulfts) v =
     | FIrrelevant -> assert (!Flags.in_debugger); mkVar(Id.of_string"_IRRELEVANT_")
     | FLOCKED -> assert (!Flags.in_debugger); mkVar(Id.of_string"_LOCKED_")
 
-and to_constr_case (lfts,_ as ulfts) ci u pms p iv c ve env =
+and to_constr_case (lfts,_ as ulfts) ci u pms (p,r) iv c ve env =
   let subs = comp_subs ulfts env in
-  let ci = usubst_case_info subs ci in
+  let r = usubst_relevance subs r in
   if is_subs_id (fst env) && is_lift_id lfts then
-    mkCase (ci, usubst_instance subs u, pms, p, iv, to_constr ulfts c, ve)
+    mkCase (ci, usubst_instance subs u, pms, (p,r), iv, to_constr ulfts c, ve)
   else
     let f_ctx (nas, c) =
       let nas = Array.map (usubst_binder subs) nas in
@@ -548,7 +543,7 @@ and to_constr_case (lfts,_ as ulfts) ci u pms p iv c ve env =
     mkCase (ci,
             usubst_instance subs u,
             Array.map (fun c -> subst_constr subs c) pms,
-            f_ctx p,
+            (f_ctx p,r),
             iv,
             to_constr ulfts c,
             Array.map f_ctx ve)
@@ -1215,8 +1210,8 @@ let rec skip_irrelevant_stack info stk = match stk with
 | (Zfix _ | Zproj _) :: s ->
   (* Typing rules ensure that fix / proj over SProp is irrelevant *)
   skip_irrelevant_stack info s
-| ZcaseT (ci, _, _, _, _, e) :: s ->
-  let r = usubst_relevance e ci.ci_relevance in
+| ZcaseT (_, _, _, (_,r), _, e) :: s ->
+  let r = usubst_relevance e r in
   if is_irrelevant info r then skip_irrelevant_stack info s
   else stk
 | Zprimitive _ :: _ -> assert false (* no irrelevant primitives so far *)
@@ -1240,9 +1235,9 @@ let rec knh info m stk =
     | FCLOS(t,e) -> knht info e t (zupdate info m stk)
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
-    | FCaseT(ci,u,pms,p,t,br,e) ->
-      let r = usubst_relevance e ci.ci_relevance in
-      if is_irrelevant info r then
+    | FCaseT(ci,u,pms,(_,r as p),t,br,e) ->
+      let r' = usubst_relevance e r in
+      if is_irrelevant info r' then
         (mk_irrelevant, skip_irrelevant_stack info stk)
       else
         knh info t (ZcaseT(ci,u,pms,p,br,e)::zupdate info m stk)
@@ -1271,13 +1266,13 @@ and knht info e t stk =
   match kind t with
     | App(a,b) ->
         knht info e a (append_stack (mk_clos_vect e b) stk)
-    | Case(ci,u,pms,p,NoInvert,t,br) ->
-      if is_irrelevant info (usubst_relevance e ci.ci_relevance) then
+    | Case(ci,u,pms,(_,r as p),NoInvert,t,br) ->
+      if is_irrelevant info (usubst_relevance e r) then
         (mk_irrelevant, skip_irrelevant_stack info stk)
       else
         knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk)
-    | Case(ci,u,pms,p,CaseInvert{indices},t,br) ->
-      if is_irrelevant info (usubst_relevance e ci.ci_relevance) then
+    | Case(ci,u,pms,(_,r as p),CaseInvert{indices},t,br) ->
+      if is_irrelevant info (usubst_relevance e r) then
         (mk_irrelevant, skip_irrelevant_stack info stk)
       else
         let term = FCaseInvert (ci, u, pms, p, (Array.map (mk_clos e) indices), mk_clos e t, br, e) in
@@ -1572,15 +1567,15 @@ and zip_term info tab m stk = match stk with
 | [] -> m
 | Zapp args :: s ->
     zip_term info tab (mkApp(m, Array.map (kl info tab) args)) s
-| ZcaseT(ci, u, pms, p, br, e) :: s ->
+| ZcaseT(ci, u, pms, (p,r), br, e) :: s ->
   let zip_ctx (nas, c) =
       let nas = Array.map (usubst_binder e) nas in
       let e = usubs_liftn (Array.length nas) e in
       (nas, klt info tab e c)
     in
-    let ci = usubst_case_info e ci in
+    let r = usubst_relevance e r in
     let u = usubst_instance e u in
-    let t = mkCase(ci, u, Array.map (fun c -> klt info tab e c) pms, zip_ctx p,
+    let t = mkCase(ci, u, Array.map (fun c -> klt info tab e c) pms, (zip_ctx p, r),
       NoInvert, m, Array.map zip_ctx br) in
     zip_term info tab t s
 | Zproj (p,r)::s ->
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c674aab25b86..d6df970398df 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -59,7 +59,6 @@ type case_info =
                                        in addition to the parameters of the related inductive type
                                        NOTE: "lets" are therefore excluded from the count
                                        NOTE: parameters of the inductive type are also excluded from the count *)
-    ci_relevance : Sorts.relevance;
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
@@ -86,7 +85,7 @@ type 'constr pcase_invert =
   | 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 'types pcase_return = (Name.t Context.binder_annot array * 'types) * Sorts.relevance
 
 type ('constr, 'types, 'univs) pcase =
   case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
@@ -495,7 +494,7 @@ let fold f acc c = match kind c with
   | App (c,l) -> Array.fold_left f (f acc c) l
   | Proj (_p,_r,c) -> f acc c
   | Evar (_,l) -> SList.Skip.fold f acc l
-  | Case (_,_,pms,(_,p),iv,c,bl) ->
+  | Case (_,_,pms,((_,p),_),iv,c,bl) ->
     Array.fold_left (fun acc (_, b) -> f acc b) (f (fold_invert f (f (Array.fold_left f acc pms) p) iv) c) bl
   | Fix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
@@ -524,7 +523,7 @@ let iter f c = match kind c with
   | Proj (_p,_r,c) -> f c
   | Evar (_,l) -> SList.Skip.iter f l
   | Case (_,_,pms,p,iv,c,bl) ->
-    Array.iter f pms; f (snd p); iter_invert f iv; f c; Array.iter (fun (_, b) -> f b) bl
+    Array.iter f pms; f (snd @@ fst p); iter_invert f iv; f c; Array.iter (fun (_, b) -> f b) bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
@@ -544,7 +543,7 @@ let iter_with_binders g f n c = match kind c with
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> SList.Skip.iter (fun c -> f n c) l
-  | Case (_,_,pms,p,iv,c,bl) ->
+  | Case (_,_,pms,(p,_),iv,c,bl) ->
     Array.Fun1.iter f n pms;
     f (iterate g (Array.length (fst p)) n) (snd p);
     iter_invert (f n) iv;
@@ -578,7 +577,7 @@ let fold_constr_with_binders g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_p,_r,c) -> f n acc c
   | Evar (_,l) -> SList.Skip.fold (f n) acc l
-  | Case (_,_,pms,p,iv,c,bl) ->
+  | Case (_,_,pms,(p,_),iv,c,bl) ->
     let fold_ctx n accu (nas, c) =
       f (iterate g (Array.length nas) n) accu c
     in
@@ -607,8 +606,9 @@ let map_branches f bl =
   let bl' = Array.map (map_under_context f) bl in
   if Array.for_all2 (==) bl' bl then bl else bl'
 
-let map_return_predicate f p =
-  map_under_context f p
+let map_return_predicate f (p,r as v) =
+  let p' = map_under_context f p in
+  if p == p' then v else p', r
 
 let map_under_context_with_binders g f l d =
   let (nas, p) = d in
@@ -620,8 +620,9 @@ let map_branches_with_binders g f l bl =
   let bl' = Array.map (map_under_context_with_binders g f l) bl in
   if Array.for_all2 (==) bl' bl then bl else bl'
 
-let map_return_predicate_with_binders g f l p =
-  map_under_context_with_binders g f l p
+let map_return_predicate_with_binders g f l (p,r as v) =
+  let p' = map_under_context_with_binders g f l p in
+  if p == p' then v else p',r
 
 let map_invert f = function
   | NoInvert -> NoInvert
@@ -710,8 +711,10 @@ let fold_map_branches f accu bl =
   let accu, bl' = Array.Smart.fold_left_map (fold_map_under_context f) accu bl in
   if Array.for_all2 (==) bl' bl then accu, bl else accu, bl'
 
-let fold_map_return_predicate f accu p =
-  fold_map_under_context f accu p
+let fold_map_return_predicate f accu (p,r as v) =
+  let accu, p' = fold_map_under_context f accu p in
+  let v = if p == p' then v else p', r in
+  accu, v
 
 let fold_map f accu c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -918,7 +921,8 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq_evars eq le
   | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
   | Construct (c1,u1), Construct (c2,u2) ->
     Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
-  | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) ->
+  | Case (ci1,u1,pms1,(p1,_r1),iv1,c1,bl1), Case (ci2,u2,pms2,(p2,_r2),iv2,c2,bl2) ->
+    (* Ignore _r1/_r2: implied by comparing p1/p2 *)
     (** 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 &&
@@ -1050,7 +1054,7 @@ let constr_ord_int f t1 t2 =
     | Ind _, _ -> -1 | _, Ind _ -> 1
     | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2
     | Construct _, _ -> -1 | _, Construct _ -> 1
-    | Case (_,_u1,pms1,p1,iv1,c1,bl1), Case (_,_u2,pms2,p2,iv2,c2,bl2) ->
+    | Case (_,_u1,pms1,(p1,_r1),iv1,c1,bl1), Case (_,_u2,pms2,(p2,_r2),iv2,c2,bl2) ->
       compare [
         (Array.compare f, pms1, pms2);
         (ctx_cmp f, p1, p2);
@@ -1153,10 +1157,10 @@ let hasheq t1 t2 =
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
     | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
     | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
-    | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) ->
+    | Case (ci1,u1,pms1,(p1,r1),iv1,c1,bl1), Case (ci2,u2,pms2,(p2,r2),iv2,c2,bl2) ->
       (** FIXME: use deeper equality for contexts *)
       u1 == u2 && array_eqeq pms1 pms2 &&
-      ci1 == ci2 && hasheq_ctx p1 p2 &&
+      ci1 == ci2 && hasheq_ctx p1 p2 && r1 == r2 &&
       invert_eqeq iv1 iv2 && c1 == c2 && Array.equal hasheq_ctx bl1 bl2
     | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
       Int.equal i1 i2
@@ -1227,8 +1231,9 @@ let rec hash t =
       combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
     | Construct (c,u) ->
       combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u))
-    | Case (_ , u, pms, p, iv, c, bl) ->
-      combinesmall 12 (combine (combine (hash c) (combine (hash_invert iv) (combine (hash_term_array pms) (combine (Instance.hash u) (hash_under_context p))))) (hash_branches bl))
+    | Case (_ , u, pms, (p,r), iv, c, bl) ->
+      combinesmall 12 (combine5 (hash c) (hash_invert iv) (hash_term_array pms) (Instance.hash u)
+                         (combine3 (hash_under_context p) (Sorts.relevance_hash r) (hash_branches bl)))
     | Fix (_ln ,(_, tl, bl)) ->
       combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
     | CoFix(_ln, (_, tl, bl)) ->
@@ -1269,7 +1274,6 @@ struct
     info1.style == info2.style
   let eq ci ci' =
     ci.ci_ind == ci'.ci_ind &&
-    ci.ci_relevance == ci'.ci_relevance &&
     Int.equal ci.ci_npar ci'.ci_npar &&
     Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
     Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *)
@@ -1293,7 +1297,7 @@ struct
     let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
     let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in
     let h5 = hash_pp_info ci.ci_pp_info in
-    combinesmall (Sorts.relevance_hash ci.ci_relevance) (combine5 h1 h2 h3 h4 h5)
+    combine5 h1 h2 h3 h4 h5
 end
 
 module Hcaseinfo = Hashcons.Make(CaseinfoHash)
@@ -1356,7 +1360,7 @@ let rec hash_term (t : t) =
     let u', hu = Instance.share u in
     (Construct (hcons_construct c, u'),
      combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu))
-  | Case (ci,u,pms,p,iv,c,bl) ->
+  | Case (ci,u,pms,(p,r),iv,c,bl) ->
     (** FIXME: use a dedicated hashconsing structure *)
     let hcons_ctx (lna, c) =
       let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in
@@ -1376,7 +1380,7 @@ let rec hash_term (t : t) =
     in
     let hbl, bl = Array.fold_left_map fold 0 bl in
     let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in
-    (Case (hcons_caseinfo ci, u, pms, p, iv, c, bl), combinesmall 12 hbl)
+    (Case (hcons_caseinfo ci, u, pms, (p,r), iv, c, bl), combinesmall 12 hbl)
   | Fix (ln,(lna,tl,bl)) ->
     let bl,hbl = hash_term_array bl in
     let tl,htl = hash_term_array tl in
@@ -1533,7 +1537,7 @@ let rec debug_print c =
   | Proj (p,_r,c) ->
     str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++
     bool (Projection.unfolded p) ++ str"," ++ debug_print c ++ str")"
-  | Case (_ci,_u,pms,p,iv,c,bl) ->
+  | Case (_ci,_u,pms,(p,_),iv,c,bl) ->
     let pr_ctx (nas, c) =
       hov 2 (hov 0 (prvect (fun na -> Name.print na.binder_name ++ spc ()) nas ++ str "|-") ++ spc () ++
         debug_print c)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 514d8cf3d09c..20febacd3600 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -45,18 +45,9 @@ type case_info =
                                        in addition to the parameters of the related inductive type
                                        NOTE: "lets" are therefore excluded from the count
                                        NOTE: parameters of the inductive type are also excluded from the count *)
-    ci_relevance : Sorts.relevance; (* relevance of the predicate (not of the inductive!) *)
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
-type 'constr pcase_invert =
-  | NoInvert
-  (** Normal reduction: match when the scrutinee is a constructor. *)
-
-  | CaseInvert of { indices : 'constr array; }
-  (** Reduce when the indices match those of the unique constructor.
-      (SProp to non SProp only) *)
-
 (** {6 The type of constructions } *)
 
 type t
@@ -165,10 +156,18 @@ end
     {e construct_args |- case_term } *)
 
 type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
+(** Names bound by matching the constructor for this branch. *)
+
+type 'types pcase_return = (Name.t Context.binder_annot array * 'types) * Sorts.relevance
 (** Names of the indices + name of self *)
 
-type 'types pcase_return = Name.t Context.binder_annot array * 'types
-(** Names of the branches *)
+type 'constr pcase_invert =
+  | NoInvert
+  (** Normal reduction: match when the scrutinee is a constructor. *)
+
+  | CaseInvert of { indices : 'constr array; }
+  (** Reduce when the indices match those of the unique constructor.
+      (SProp to non SProp only) *)
 
 type ('constr, 'types, 'univs) pcase =
   case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
diff --git a/kernel/conversion.ml b/kernel/conversion.ml
index 4441913b390c..0e277f999e29 100644
--- a/kernel/conversion.ml
+++ b/kernel/conversion.ml
@@ -844,7 +844,7 @@ and convert_return_clause mib mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu
       let ctx = LocalAssum (Context.anonR, dummy) :: ctx in
       Some (ctx, u1, u2, pms1, pms2)
   in
-  convert_under_context l2r infos e1 e2 l1 l2 ctx p1 p2 cu
+  convert_under_context l2r infos e1 e2 l1 l2 ctx (fst p1) (fst p2) cu
 
 and convert_branches mib mip l2r infos e1 e2 lft1 lft2 u1 u2 pms1 pms2 br1 br2 cuniv =
   let fold i (ctx, _) cuniv =
diff --git a/kernel/genlambda.ml b/kernel/genlambda.ml
index f2b1d9df3d29..22723ad67f44 100644
--- a/kernel/genlambda.ml
+++ b/kernel/genlambda.ml
@@ -636,7 +636,7 @@ let rec lambda_of_constr cache env sigma c =
     Lproj (Projection.repr p, c)
 
   | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
-    let (ci, t, _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in
+    let (ci, (t,_), _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in
     let (mind, i) = ci.ci_ind in
     let mib = lookup_mind mind env in
     let oib = mib.mind_packets.(i) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d84b6e42a208..a1a40d97db68 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -356,7 +356,12 @@ let expand_arity (mib, mip) (ind, u) params nas =
   let realdecls = LocalAssum (na, self) :: realdecls in
   instantiate_context u params nas realdecls
 
-let expand_case_specif mib (ci, u, params, p, iv, c, br) =
+type ('constr,'types) pexpanded_case =
+  (case_info * ('constr * Sorts.relevance) * 'constr pcase_invert * 'constr * 'constr array)
+
+type expanded_case = (constr,types) pexpanded_case
+
+let expand_case_specif mib (ci, u, params, (p,rp), iv, c, br) =
   (* Γ ⊢ c : I@{u} params args *)
   (* Γ, indices, self : I@{u} params indices ⊢ p : Type *)
   let mip = mib.mind_packets.(snd ci.ci_ind) in
@@ -377,13 +382,13 @@ let expand_case_specif mib (ci, u, params, p, iv, c, br) =
     in
     Array.map2_i build_one_branch br mip.mind_nf_lc
   in
-  (ci, ep, iv, c, ebr)
+  (ci, (ep,rp), iv, c, ebr)
 
 let expand_case env (ci, _, _, _, _, _, _ as case) =
   let specif = Environ.lookup_mind (fst ci.ci_ind) env in
   expand_case_specif specif case
 
-let contract_case env (ci, p, iv, c, br) =
+let contract_case env (ci, (p,rp), iv, c, br) =
   let (mib, mip) = lookup_mind_specif env ci.ci_ind in
   let (arity, p) = Term.decompose_lambda_n_decls (mip.mind_nrealdecls + 1) p in
   let (u, pms) = match arity with
@@ -401,7 +406,7 @@ let contract_case env (ci, p, iv, c, br) =
   in
   let p =
     let nas = Array.of_list (List.rev_map get_annot arity) in
-    (nas, p)
+    ((nas, p),rp)
   in
   let map i br =
     let (ctx, br) = Term.decompose_lambda_n_decls mip.mind_consnrealdecls.(i) br in
@@ -434,14 +439,13 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
 (************************************************************************)
 (* Checking the case annotation is relevant *)
 
-let check_case_info env (indsp,u) r ci =
+let check_case_info env (indsp,u) ci =
   let (mib,mip as spec) = lookup_mind_specif env indsp in
   if
     not (QInd.equal env indsp ci.ci_ind) ||
     not (Int.equal mib.mind_nparams ci.ci_npar) ||
     not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) ||
     not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) ||
-    not (Sorts.relevance_equal ci.ci_relevance r) ||
     is_primitive_record spec
   then raise (TypeError(env,WrongCaseInfo((indsp,u),ci)))
 
@@ -905,7 +909,7 @@ let rec subterm_specif renv stack t =
     match kind f with
     | Rel k -> subterm_var k renv
     | Case (ci, u, pms, p, iv, c, lbr) -> (* iv ignored: it's just a cache *)
-      let (ci, p, _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in
+      let (ci, (p,_), _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in
        let stack' = push_stack_closures renv l stack in
        let cases_spec =
          branches_specif renv (lazy_subterm_specif renv [] c) ci
@@ -1164,7 +1168,7 @@ let check_one_fix renv recpos trees def =
             end
 
         | Case (ci, u, pms, ret, iv, c_0, br) -> (* iv ignored: it's just a cache *)
-            let (ci, p, _iv, c_0, brs) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in
+            let (ci, (p,_), _iv, c_0, brs) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in
             let needreduce_c_0, rs = check_rec_call renv rs c_0 in
             let rs = check_inert_subterm_rec_call renv rs p in
             (* compute the recarg info for the arguments of each branch *)
@@ -1536,7 +1540,7 @@ let check_one_cofix env nbfix def deftype =
 
         | Case (ci, u, pms, p, iv, tm, br) -> (* iv ignored: just a cache *)
           begin
-            let (_, p, _iv, tm, vrest) = expand_case env (ci, u, pms, p, iv, tm, br) in
+            let (_, (p,_), _iv, tm, vrest) = expand_case env (ci, u, pms, p, iv, tm, br) in
             let tree = match restrict_spec env (Subterm (Int.Set.empty, Strict, tree)) p with
             | Dead_code -> assert false
             | Subterm (_, _, tree') -> tree'
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 049618b00734..4a17b5f6f956 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -95,16 +95,21 @@ val inductive_params : mind_specif -> int
 val expand_arity : mind_specif -> pinductive -> constr array ->
   Name.t Context.binder_annot array -> rel_context
 
+type ('constr,'types) pexpanded_case =
+  (case_info * ('constr * Sorts.relevance) * 'constr pcase_invert * 'constr * 'constr array)
+
+type expanded_case = (constr,types) pexpanded_case
+
 (** Given a pattern-matching represented compactly, expands it so as to produce
     lambda and let abstractions in front of the return clause and the pattern
     branches. *)
-val expand_case : env -> case -> (case_info * constr * case_invert * constr * constr array)
+val expand_case : env -> case -> expanded_case
 
-val expand_case_specif : mutual_inductive_body -> case -> (case_info * constr * case_invert * constr * constr array)
+val expand_case_specif : mutual_inductive_body -> case -> expanded_case
 
 (** Dual operation of the above. Fails if the return clause or branch has not
     the expected form. *)
-val contract_case : env -> (case_info * constr * case_invert * constr * constr array) -> case
+val contract_case : env -> expanded_case -> case
 
 (** [instantiate_context u subst nas ctx] applies both [u] and [subst]
     to [ctx] while replacing names using [nas] (order reversed). In particular,
@@ -123,7 +128,7 @@ val inductive_sort_family : one_inductive_body -> Sorts.family
 
 (** Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
-val check_case_info : env -> pinductive -> Sorts.relevance -> case_info -> unit
+val check_case_info : env -> pinductive -> case_info -> unit
 
 (** {6 Guard conditions for fix and cofix-points. } *)
 
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 7f7a2d968097..e899f096174f 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -252,7 +252,9 @@ let rec infer_fterm cv_pb infos variances hd stk =
 
   | FCaseInvert (ci, u, pms, p, _, _, br, e) ->
     let mib = Environ.lookup_mind (fst ci.ci_ind) (info_env (fst infos)) in
-    let (_, p, _, _, br) = Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br) in
+    let (_, (p, _), _, _, br) =
+      Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br)
+    in
     let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in
     let variances = infer p variances in
     Array.fold_right infer br variances
@@ -275,7 +277,7 @@ and infer_stack infos variances (stk:CClosure.stack) =
       | ZcaseT (ci,u,pms,p,br,e) ->
         let dummy = mkProp in
         let case = (ci, u, pms, p, NoInvert, dummy, br) in
-        let (_, p, _, _, br) = Inductive.expand_case (info_env (fst infos)) case in
+        let (_, (p, _), _, _, br) = Inductive.expand_case (info_env (fst infos)) case in
         let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
         infer_vect infos variances (Array.map (mk_clos e) br)
       | Zshift _ -> variances
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ef667e9133a6..d75b685bcdc9 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -355,7 +355,7 @@ let rec map_kn f f' c =
       | Construct (((kn,i),j),u) ->
           let kn' = f kn in
           if kn'==kn then c else mkConstructU (((kn',i),j),u)
-      | Case (ci,u,pms,p,iv,ct,l) ->
+      | Case (ci,u,pms,(p,r),iv,ct,l) ->
           let ci_ind =
             let (kn,i) = ci.ci_ind in
             let kn' = f kn in
@@ -374,7 +374,7 @@ let rec map_kn f f' c =
                 && l'==l && ct'==ct)then c
             else
               mkCase ({ci with ci_ind = ci_ind}, u,
-                      pms',p',iv',ct', l')
+                      pms',(p',r),iv',ct', l')
       | Cast (ct,k,t) ->
           let ct' = func ct in
           let t'= func t in
diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml
index 435776f00ac8..36517e877c5a 100644
--- a/kernel/relevanceops.ml
+++ b/kernel/relevanceops.ml
@@ -61,7 +61,7 @@ let rec relevance_of_term_extra env extra lft c =
   | App (c, _) -> relevance_of_term_extra env extra lft c
   | Const c -> relevance_of_constant env c
   | Construct c -> relevance_of_constructor env c
-  | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
+  | Case (_, _, _, (_, r), _, _, _) -> r
   | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (_, r, _) -> r
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6c460fc6c3bb..c59e2ee9e919 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -493,8 +493,8 @@ let check_branch_types env (_mib, mip) ci u pms c _ct lft (pctx, p) =
     let expbrt = it_mkLambda_or_LetIn expbrt brctx in
     error_ill_formed_branch env c ((ci.ci_ind, i + 1), u) brt expbrt
 
-let should_invert_case env ci =
-  Sorts.relevance_equal ci.ci_relevance Sorts.Relevant &&
+let should_invert_case env r ci =
+  Sorts.relevance_equal r Sorts.Relevant &&
   let mib,mip = lookup_mind_specif env ci.ci_ind in
   Sorts.relevance_equal mip.mind_relevance Sorts.Irrelevant &&
   (* NB: it's possible to have 2 ctors or arguments to 1 ctor by unsetting univ checks
@@ -523,7 +523,7 @@ let type_case_scrutinee env (mib, _mip) (u', largs) u pms (pctx, p) c =
   let subst = Vars.subst_of_rel_context_instance_list pctx (realargs @ [c]) in
   Vars.substl subst p
 
-let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, pt) iv c ct lf lft =
+let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, rp, pt) iv c ct lf lft =
   let ((ind, u'), largs) =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct) in
@@ -534,20 +534,20 @@ let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, pt) iv c ct l
   | exception DestKO ->
     error_elim_arity env (ind, u') c None
   in
-  let rp = Sorts.relevance_of_sort sp in
-  let ci =
-    if Sorts.relevance_equal ci.ci_relevance rp then ci
+  let rp =
+    let expected = Sorts.relevance_of_sort sp in
+    if Sorts.relevance_equal rp expected then rp
     else
-      let () = warn_bad_relevance_case env rp (ci, u, pms, (pnas, p), iv, c, lf) in
-      {ci with ci_relevance=rp}
+      let () = warn_bad_relevance_case env expected (ci, u, pms, ((pnas, p), rp), iv, c, lf) in
+      expected
   in
-  let () = check_case_info env (ind, u') rp ci in
+  let () = check_case_info env (ind, u') ci in
   let () =
     let is_inversion = match iv with
       | NoInvert -> false
       | CaseInvert _ -> true (* contents already checked *)
     in
-    if not (is_inversion = should_invert_case env ci)
+    if not (is_inversion = should_invert_case env rp ci)
     then error_bad_invert env
   in
   let () =
@@ -563,7 +563,7 @@ let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, pt) iv c ct l
   (* We return the "higher" inductive universe instance from the predicate,
      the branches must be typeable using these universes. *)
   let () = check_branch_types env (mib, mip) ci u pms c ct lft (pctx, p) in
-  ci, rslty
+  rp, rslty
 
 let type_of_projection env p c ct =
   let pr, pty = lookup_projection p env in
@@ -721,7 +721,7 @@ let rec execute env cstr =
     | Construct c ->
       cstr, type_of_constructor env c
 
-    | Case (ci, u, pms, p, iv, c, lf) ->
+    | Case (ci, u, pms, (p,rp), iv, c, lf) ->
         let c', ct = execute env c in
         let iv' = match iv with
           | NoInvert -> NoInvert
@@ -781,10 +781,10 @@ let rec execute env cstr =
           if br == br' then b else (nas, br')
         in
         let lf' = Array.Smart.map_i build_one_branch lf in
-        let ci', t = type_of_case env (mib, mip) ci u pms' (pctx, fst p, p', pt) iv' c' ct lf' lft in
+        let rp', t = type_of_case env (mib, mip) ci u pms' (pctx, fst p, p', rp, pt) iv' c' ct lf' lft in
         let eqbr (_, br1) (_, br2) = br1 == br2 in
-        let cstr = if ci == ci' && pms == pms' && c == c' && snd p == p' && iv == iv' && Array.equal eqbr lf lf' then cstr
-          else mkCase (ci', u, pms', (fst p, p'), iv', c', lf')
+        let cstr = if rp == rp' && pms == pms' && c == c' && snd p == p' && iv == iv' && Array.equal eqbr lf lf' then cstr
+          else mkCase (ci, u, pms', ((fst p, p'), rp'), iv', c', lf')
         in
         cstr, t
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index de7fb4a37677..dad1a8238021 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -135,6 +135,6 @@ type ('constr,'types) bad_relevance =
 val bad_relevance_msg : (env * (constr,types) bad_relevance) CWarnings.msg
 (** Used by the higher layers to register a nicer printer than the default. *)
 
-val should_invert_case : env -> case_info -> bool
+val should_invert_case : env -> Sorts.relevance -> case_info -> bool
 (** We have case inversion exactly when going from irrelevant nonempty
    (ie 1 constructor) inductive to relevant type. *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 1bd44cdab4fb..b2aed026c300 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -281,11 +281,6 @@ let map_annot_relevance f na =
   let r' = f r in
   if r' == r then na else { na with binder_relevance = r' }
 
-let map_case_info_relevance f ci =
-  let r = ci.ci_relevance in
-  let r' = f r in
-  if r' == r then ci else { ci with ci_relevance = r' }
-
 let map_case_under_context_relevance f (nas,x as v) =
   let nas' = CArray.Smart.map (map_annot_relevance f) nas in
   if nas' == nas then v else (nas',x)
@@ -313,12 +308,12 @@ let map_constr_relevance f c =
     let na' = map_annot_relevance f na in
     if na' == na then c else mkLetIn (na',x,y,z)
 
-  | Case (ci,u,params,ret,iv,v,brs) ->
-    let ci' = map_case_info_relevance f ci in
+  | Case (ci,u,params,(ret,r),iv,v,brs) ->
+    let r' = f r in
     let ret' = map_case_under_context_relevance f ret in
     let brs' = CArray.Smart.map (map_case_under_context_relevance f) brs in
-    if ci' == ci && ret' == ret && brs' == brs then c
-    else mkCase (ci',u,params,ret',iv,v,brs')
+    if r' == r && ret' == ret && brs' == brs then c
+    else mkCase (ci,u,params,(ret',r'),iv,v,brs')
 
   | Fix data ->
     let data' = map_rec_declaration_relevance f data in
@@ -351,8 +346,8 @@ let fold_constr_relevance f acc c =
   | Prod (na,_,_) | Lambda (na,_,_) | LetIn (na,_,_,_) ->
     fold_annot_relevance f acc na
 
-  | Case (ci,_u,_params,ret,_iv,_v,brs) ->
-    let acc = f acc ci.ci_relevance in
+  | Case (_,_u,_params,(ret,r),_iv,_v,brs) ->
+    let acc = f acc r in
     let acc = fold_case_under_context_relevance f acc ret in
     let acc = CArray.fold_left (fold_case_under_context_relevance f) acc brs in
     acc
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4dac0ba0a577..c72539376c97 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1075,10 +1075,10 @@ let fake_match_projection env p =
     ci_npar = mib.mind_nparams;
     ci_cstr_ndecls = mip.mind_consnrealdecls;
     ci_cstr_nargs = mip.mind_consnrealargs;
-    ci_relevance = relevance_of_projection_repr mib p;
     ci_pp_info;
   }
   in
+  let relevance = relevance_of_projection_repr mib p in
   let x = match mib.mind_record with
     | NotRecord | FakeRecord -> assert false
     | PrimRecord info ->
@@ -1101,7 +1101,7 @@ let fake_match_projection env p =
           (nas, mkRel (List.length ctx - (j - 1)))
         in
         let params = Context.Rel.instance mkRel 1 paramslet in
-        let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
+        let body = mkCase (ci, u, params, (p,relevance), NoInvert, mkRel 1, [|branch|]) in
         it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
     | LocalDef (_,c,t) :: rem ->
       let c = liftn 1 j c in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index a7e41222dfef..2c2be2267845 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -69,8 +69,8 @@ let unif env evd t1 t2=
               Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
           | Case (cia,ua,pmsa,pa,iva,ca,va),Case (cib,ub,pmsb,pb,ivb,cb,vb)->
             let env = Global.env () in
-            let (cia,pa,iva,ca,va) = EConstr.expand_case env evd (cia,ua,pmsa,pa,iva,ca,va) in
-            let (cib,pb,iva,cb,vb) = EConstr.expand_case env evd (cib,ub,pmsb,pb,ivb,cb,vb) in
+            let (cia,(pa,_),iva,ca,va) = EConstr.expand_case env evd (cia,ua,pmsa,pa,iva,ca,va) in
+            let (cib,(pb,_),iva,cb,vb) = EConstr.expand_case env evd (cib,ub,pmsb,pb,ivb,cb,vb) in
               Queue.add (pa,pb) bige;
               Queue.add (ca,cb) bige;
               let l=Array.length va in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3001dbcbd539..ae8e8e1aba88 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -293,7 +293,7 @@ let check_not_nested env sigma forbidden e =
     | Const _ -> ()
     | Ind _ -> ()
     | Construct _ -> ()
-    | Case (_, _, pms, (_, t), _, e, a) ->
+    | Case (_, _, pms, ((_, t), _), _, e, a) ->
       Array.iter check_not_nested pms;
       check_not_nested t;
       check_not_nested e;
@@ -359,7 +359,7 @@ type journey_info =
           -> constr infos
           -> unit Proofview.tactic)
       -> ( case_info
-           * constr
+           * (constr * Sorts.relevance)
            * case_invert
            * constr
            * constr array
@@ -766,7 +766,7 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
         try
           check_not_nested env sigma
             (expr_info.f_id :: expr_info.forbidden_ids)
-            a;
+            (fst a);
           false
         with e when CErrors.noncritical e -> true
       in
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index f7792eeeeb0f..ba23f7847590 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -526,7 +526,7 @@ let () =
     let (ci, c, iv, t, bl) = EConstr.expand_case env sigma (ci, u, pms, c, iv, t, bl) in
     v_blk 13 [|
       Tac2ffi.of_ext Tac2ffi.val_case ci;
-      Tac2ffi.of_constr c;
+      Tac2ffi.(of_pair of_constr of_relevance c);
       of_case_invert iv;
       Tac2ffi.of_constr t;
       Tac2ffi.of_array Tac2ffi.of_constr bl;
@@ -619,7 +619,7 @@ let () =
     EConstr.mkConstructU (cstr, u)
   | (13, [|ci; c; iv; t; bl|]) ->
     let ci = Tac2ffi.to_ext Tac2ffi.val_case ci in
-    let c = Tac2ffi.to_constr c in
+    let c = Tac2ffi.(to_pair to_constr to_relevance c) in
     let iv = to_case_invert iv in
     let t = Tac2ffi.to_constr t in
     let bl = Tac2ffi.to_array Tac2ffi.to_constr bl in
@@ -691,7 +691,7 @@ let () =
   define "constr_case" (inductive @-> tac valexpr) @@ fun ind ->
   Proofview.tclENV >>= fun env ->
   try
-    let ans = Inductiveops.make_case_info env ind Sorts.Relevant Constr.RegularStyle in
+    let ans = Inductiveops.make_case_info env ind Constr.RegularStyle in
     return (Tac2ffi.of_ext Tac2ffi.val_case ans)
   with e when CErrors.noncritical e ->
     throw err_notfound
@@ -804,8 +804,7 @@ let () =
 let () =
   let ty = repr_ext val_case in
   define "constr_case_equal" (ty @-> ty @-> ret bool) @@ fun x y ->
-  Ind.UserOrd.equal x.ci_ind y.ci_ind &&
-  Sorts.relevance_equal x.ci_relevance y.ci_relevance
+  Ind.UserOrd.equal x.ci_ind y.ci_ind
 let () =
   let ty = repr_ext val_constructor in
   define "constructor_equal" (ty @-> ty @-> ret bool) Construct.UserOrd.equal
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4226215d6d7f..f22a5c740f2e 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -272,7 +272,7 @@ let iter_constr_LR sigma f c = match EConstr.kind sigma c with
   | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
   | LetIn (_, v, t, b) -> f v; f t; f b
   | App (cf, a) -> f cf; Array.iter f a
-  | Case (_, _, pms, (_, p), iv, v, b) ->
+  | Case (_, _, pms, ((_, p), _), iv, v, b) ->
     f v; Array.iter f pms; f p; iter_invert f iv; Array.iter (fun (_, c) -> f c) b
   | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 528e608bc688..740bfd4eb093 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1162,7 +1162,7 @@ let rec ungeneralize sigma n ng body =
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
       mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c)
-  | Case (ci,u,pms,p,iv,c,brs) ->
+  | Case (ci,u,pms,(p,rp),iv,c,brs) ->
       (* We traverse a split *)
       let p =
         let (nas, p) = p in
@@ -1171,7 +1171,7 @@ let rec ungeneralize sigma n ng body =
         nas, it_mkProd_or_LetIn p sign2
       in
       let map (nas, br) = nas, ungeneralize sigma (n + Array.length nas) ng br in
-      mkCase (ci, u, pms, p, iv, c, Array.map map brs)
+      mkCase (ci, u, pms, (p,rp), iv, c, Array.map map brs)
   | App (f,args) ->
       (* We traverse an inner generalization *)
       assert (isCase sigma f);
@@ -1479,9 +1479,9 @@ let compile ~program_mode sigma pb =
                 pred current indt (names,dep) tomatch
             in
             let rci = Typing.check_allowed_sort !!(pb.env) sigma mind current pred in
-            let ci = make_case_info !!(pb.env) (fst mind) rci pb.casestyle in
+            let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
             let pred = nf_betaiota !!(pb.env) sigma pred in
-            let case = make_case_or_project !!(pb.env) sigma indt ci pred current brvals in
+            let case = make_case_or_project !!(pb.env) sigma indt ci (pred,rci) current brvals in
             let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
             let used = List.flatten (Array.to_list used) in
             used, sigma, { uj_val = applist (case, inst);
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 0ed0d7824916..9ade0f08ddbe 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -692,7 +692,7 @@ let rec apply_stack info t = function
       apply_stack info (mkApp(t,Array.map_of_list (cbv_norm_value info) args)) st
   | CASE (u,pms,ty,br,iv,ci,env,st) ->
     (* FIXME: Prevent this expansion by caching whether an inductive contains let-bindings *)
-    let (_, ty, _, _, br) = Inductive.expand_case info.env (ci, u, pms, ty, iv, mkProp, br) in
+    let (_, (ty,r), _, _, br) = Inductive.expand_case info.env (ci, u, pms, ty, iv, mkProp, br) in
     let ty =
       let (_, mip) = Inductive.lookup_mind_specif info.env ci.ci_ind in
       Term.decompose_lambda_n_decls (mip.Declarations.mind_nrealdecls + 1) ty
@@ -713,7 +713,7 @@ let rec apply_stack info t = function
       (nas, cbv_norm_term info env c)
     in
       apply_stack info
-        (mkCase (ci, u, Array.map (cbv_norm_term info env) pms, map_ctx ty, iv, t,
+        (mkCase (ci, u, Array.map (cbv_norm_term info env) pms, (map_ctx ty,r), iv, t,
                     Array.map map_ctx br))
         st
   | PROJ (p, r, st) ->
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3590503a0d4a..525f89f62872 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -405,7 +405,7 @@ let matches_core env sigma allow_bound_rels
             raise PatternMatchingFailure
 
       | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
-          let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
+          let (_, _, _, (p2,_), _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
           let n2 = Array.length br2 in
           let () = match ci1.cip_ind with
           | None -> ()
@@ -577,7 +577,7 @@ let sub_match ?(closed=true) env sigma pat c =
      try_aux [(env, app); (env, Array.last lc)] mk_ctx next
   | Case (ci,u,pms,hd0,iv,c1,lc0) ->
       let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
-      let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
+      let (_, (hd,hdr), _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
       let hd =
         let (ctx, hd) = decompose_lambda_decls sigma hd in
         (push_rel_context ctx env, hd)
@@ -593,9 +593,9 @@ let sub_match ?(closed=true) env sigma pat c =
         let pms, rem = List.chop (Array.length pms) rem in
         let pms = Array.of_list pms in
         let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in
-        let hd = (fst hd0, hd) in
+        let hd = (fst (fst hd0), hd) in
         let map_br (nas, _) br = (nas, br) in
-        mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
+        mk_ctx (mkCase (ci,u,pms,(hd,hdr),iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
       | _ -> assert false
       in
       let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 072ee3d6a03a..e7b4cbab2eaa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -66,7 +66,7 @@ let instantiate_context u subst nas ctx =
   let () = if not (Int.equal (Array.length nas) (List.length ctx)) then raise_notrace Exit in
   instantiate (Array.length nas - 1) ctx
 
-let return_clause env sigma ind u params (nas, p) =
+let return_clause env sigma ind u params ((nas, p),_) =
   try
     let u = EConstr.Unsafe.to_instance u in
     let params = EConstr.Unsafe.to_constr_array params in
@@ -519,7 +519,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | [] -> [Id.Set.empty,[],rhs]
   | na::nal ->
     match EConstr.kind sigma c with
-    | Case (ci,u,pms,p,iv,c,cl) when
+    | Case (ci,u,pms,(p,_),iv,c,cl) when
         eq_constr (snd (snd e)) sigma c (mkRel (List.index Name.equal na (fst (snd e))))
         && not (Int.equal (Array.length cl) 0)
         && (* don't contract if p dependent *)
@@ -953,7 +953,7 @@ and detype_r d flags avoid env sigma t =
     | Construct (cstr_sp,u) ->
         GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,u,pms,p,iv,c,bl) ->
-        let comp = computable sigma p in
+        let comp = computable sigma (fst p) in
         let case = (ci, u, pms, p, iv, c, bl) in
         detype_case comp (detype d flags avoid env sigma)
           (detype_eqns d flags avoid env sigma comp)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 664a7a4f9636..b1336af1a997 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -449,8 +449,8 @@ let rec ise_stack2 no_app env evd f sk1 sk2 =
     match revsk1, revsk2 with
     | [], [] -> None, Success i
     | Stack.Case cse1 :: q1, Stack.Case cse2 :: q2 ->
-      let (ci1, u1, pms1, t1, br1) = Stack.expand_case env evd cse1 in
-      let (ci2, u2, pms2, t2, br2) = Stack.expand_case env evd cse2 in
+      let (ci1, u1, pms1, (t1,_), br1) = Stack.expand_case env evd cse1 in
+      let (ci2, u2, pms2, (t2,_), br2) = Stack.expand_case env evd cse2 in
       let hd1 = mkIndU (ci1.ci_ind, u1) in
       let hd2 = mkIndU (ci2.ci_ind, u2) in
       let fctx i (ctx1, t1) (_ctx2, t2) = f (push_rel_context ctx1 env) i CONV t1 t2 in
@@ -494,8 +494,8 @@ let rec exact_ise_stack2 env evd f sk1 sk2 =
     match revsk1, revsk2 with
     | [], [] -> Success i
     | Stack.Case cse1 :: q1, Stack.Case cse2 :: q2 ->
-      let (ci1, u1, pms1, t1, br1) = Stack.expand_case env evd cse1 in
-      let (ci2, u2, pms2, t2, br2) = Stack.expand_case env evd cse2 in
+      let (ci1, u1, pms1, (t1,_), br1) = Stack.expand_case env evd cse1 in
+      let (ci2, u2, pms2, (t2,_), br2) = Stack.expand_case env evd cse2 in
       let hd1 = mkIndU (ci1.ci_ind, u1) in
       let hd2 = mkIndU (ci2.ci_ind, u2) in
       let fctx i (ctx1, t1) (_ctx2, t2) = f (push_rel_context ctx1 env) i CONV t1 t2 in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d6446cca5b36..dfb2df2cbfc4 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -192,8 +192,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib, mip) kind =
     let depind = build_dependent_inductive !!env indf' in
     let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in
 
-    let rci = relevance in
-    let ci = make_case_info !!env (fst pind) rci RegularStyle in
+    let ci = make_case_info !!env (fst pind) RegularStyle in
     let pbody =
       appvect
         (mkRel (ndepar + nbprod),
@@ -209,7 +208,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib, mip) kind =
       | None ->
         let pms = Context.Rel.instance mkRel (ndepar + nbprod) lnamespar in
         let iv =
-          if Typeops.should_invert_case !!env ci then
+          if Typeops.should_invert_case !!env relevance ci then
             CaseInvert { indices = Context.Rel.instance mkRel 1 arsign }
           else NoInvert
         in
@@ -225,7 +224,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib, mip) kind =
         in
         let br = Array.init ncons mk_branch in
         let pnas = Array.of_list (List.rev_map get_annot pctx) in
-        let obj = mkCase (ci, u, pms, (pnas, liftn ndepar (ndepar + 1) pbody), iv, mkRel 1, br) in
+        let obj = mkCase (ci, u, pms, ((pnas, liftn ndepar (ndepar + 1) pbody), relevance), iv, mkRel 1, br) in
         sigma, obj, pbody
       | Some ps ->
         let term =
@@ -503,8 +502,7 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
             (* body of i-th component of the mutual fixpoint *)
             let target_relevance = Sorts.relevance_of_sort_family target_sort in
             let deftyi =
-              let rci = target_relevance in
-              let ci = make_case_info !!env indi rci RegularStyle in
+              let ci = make_case_info !!env indi RegularStyle in
               let concl = applist (mkRel (dect+j+ndepar),pargs) in
               let pred =
                 it_mkLambda_or_LetIn_name env
@@ -514,8 +512,9 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
               in
               let obj =
                 let indty = find_rectype !!env sigma (EConstr.of_constr depind) in
-                Inductiveops.make_case_or_project !!env !evdref indty ci (EConstr.of_constr pred)
-                                                  (EConstr.mkRel 1) (Array.map EConstr.of_constr branches)
+                Inductiveops.make_case_or_project !!env !evdref indty ci
+                  (EConstr.of_constr pred, target_relevance)
+                  (EConstr.mkRel 1) (Array.map EConstr.of_constr branches)
               in
               let obj = EConstr.to_constr !evdref obj in
                 it_mkLambda_or_LetIn_name env obj
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23047eeb4e69..5dc8a8294a1b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -243,7 +243,7 @@ let has_dependent_elim (mib,mip) =
   | NotRecord | FakeRecord -> true
 
 (* Annotation for cases *)
-let make_case_info env ind r style =
+let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let ind_tags =
     Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
@@ -256,7 +256,6 @@ let make_case_info env ind r style =
     ci_npar    = mib.mind_nparams;
     ci_cstr_ndecls = mip.mind_consnrealdecls;
     ci_cstr_nargs = mip.mind_consnrealargs;
-    ci_relevance = r;
     ci_pp_info = print_info }
 
 (*s Useful functions *)
@@ -310,8 +309,8 @@ let get_constructors env (ind,params) =
 
 let get_projections = Environ.get_projections
 
-let make_case_invert env (IndType (((ind,u),params),indices)) ci =
-  if Typeops.should_invert_case env ci
+let make_case_invert env (IndType (((ind,u),params),indices)) ~case_relevance:r ci =
+  if Typeops.should_invert_case env r ci
   then CaseInvert {indices=Array.of_list indices}
   else NoInvert
 
@@ -374,7 +373,7 @@ let simple_make_case_or_project env sigma ci pred invert c branches =
   let projs = get_projections env ind in
   match projs with
   | None -> mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches))
-  | Some ps -> make_project env sigma ind pred c branches ps
+  | Some ps -> make_project env sigma ind (fst pred) c branches ps
 
 let make_case_or_project env sigma indt ci pred c branches =
   let open EConstr in
@@ -382,9 +381,9 @@ let make_case_or_project env sigma indt ci pred c branches =
   let projs = get_projections env ind in
   match projs with
   | None ->
-     let invert = make_case_invert env indt ci in
+     let invert = make_case_invert env indt ~case_relevance:(snd pred) ci in
      mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches))
-  | Some ps -> make_project env sigma ind pred c branches ps
+  | Some ps -> make_project env sigma ind (fst pred) c branches ps
 
 (* substitution in a signature *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 0437ce4b47df..4668ee495554 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -177,7 +177,7 @@ val arity_of_case_predicate :
   env -> inductive_family -> bool -> Sorts.t -> types
 
 (** Annotation for cases *)
-val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info
+val make_case_info : env -> inductive -> case_style -> case_info
 
 (** Make a case or substitute projections if the inductive type is a record
     with primitive projections.
@@ -185,15 +185,15 @@ val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_i
     inductive type does not allow dependent elimination. *)
 val make_case_or_project :
   env -> evar_map -> inductive_type -> case_info ->
-  (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
+  (* pred *) EConstr.constr * Sorts.relevance -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
 
 (** Sometimes [make_case_or_project] is nicer to call with a pre-built
    [case_invert] than [inductive_type]. *)
 val simple_make_case_or_project :
   env -> evar_map -> case_info ->
-  (* pred *) EConstr.constr -> EConstr.case_invert -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
+  (* pred *) EConstr.constr * Sorts.relevance -> EConstr.case_invert -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
 
-val make_case_invert : env -> inductive_type -> case_info
+val make_case_invert : env -> inductive_type -> case_relevance:Sorts.relevance -> case_info
   -> EConstr.case_invert
 
 (*i Compatibility
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 901164f0fe37..a04ae35c131b 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -338,12 +338,12 @@ and nf_atom_type env sigma atom =
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type (pctx, p) realargs a in
       let p = (get_case_annot pctx, p) in
-      let ci = Inductiveops.make_case_info env ind relevance RegularStyle in
-      let iv = if Typeops.should_invert_case env ci then
+      let ci = Inductiveops.make_case_info env ind RegularStyle in
+      let iv = if Typeops.should_invert_case env relevance ci then
           CaseInvert {indices=realargs}
         else NoInvert
       in
-      mkCase (ci, u, params, p, iv, a, branchs), tcase
+      mkCase (ci, u, params, (p,relevance), iv, a, branchs), tcase
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
       let tt = Array.map fst tt and rt = Array.map snd tt in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ac2283d93db7..31592bcb914d 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -187,14 +187,14 @@ let pattern_of_constr ~broken env sigma t =
       | _ ->
         PMeta None)
     | Case (ci, u, pms, p0, iv, a, br0) ->
-        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in
+        let (ci, (p,_), iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in
         let pattern_of_ctx c (nas, c0) =
           let ctx, c = Term.decompose_lambda_n_decls (Array.length nas) c in
           let env = push_rel_context ctx env in
           let c = pattern_of_constr env c in
           (Array.map Context.binder_name nas, c)
         in
-        let p = pattern_of_ctx p p0 in
+        let p = pattern_of_ctx p (fst p0) in
         let cip =
           { cip_style = ci.ci_pp_info.style;
             cip_ind = Some ci.ci_ind;
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 407b27c6f7e5..89968c052f83 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -77,6 +77,11 @@ exception PretypeError of env * Evd.evar_map * pretype_error
 val precatchable_exception : exn -> bool
 
 (** Raising errors *)
+val raise_type_error
+  : ?loc:Loc.t
+  -> Environ.env * Evd.evar_map * type_error
+  -> 'a
+
 val error_actual_type :
   ?loc:Loc.t -> ?info:Exninfo.info -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
       unification_error -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 253bcef7f2ae..19dc9a709a99 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1142,8 +1142,8 @@ struct
     let obj indt rci p v f =
       if not record then
         let f = it_mkLambda_or_LetIn f fsign in
-        let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in
-          mkCase (EConstr.contract_case !!env sigma (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]))
+        let ci = make_case_info !!env (ind_of_ind_type indt) LetStyle in
+          mkCase (EConstr.contract_case !!env sigma (ci, (p,rci), make_case_invert !!env indt ~case_relevance:rci ci, cj.uj_val,[|f|]))
       else it_mkLambda_or_LetIn f fsign
     in
     (* Make dependencies from arity signature impossible *)
@@ -1259,8 +1259,11 @@ struct
         let ind,_ = dest_ind_family indf in
         let pred = nf_evar sigma pred in
         let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in
-        let ci = make_case_info !!env (fst ind) rci IfStyle in
-        mkCase (EConstr.contract_case !!env sigma (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]))
+        let ci = make_case_info !!env (fst ind) IfStyle in
+        mkCase (EConstr.contract_case !!env sigma
+                  (ci, (pred,rci),
+                   make_case_invert !!env indty ~case_relevance:rci ci, cj.uj_val,
+                   [|b1;b2|]))
       in
       let cj = { uj_val = v; uj_type = p } in
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma cj tycon
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 204dc4318a77..2d89455ce8ab 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -215,7 +215,7 @@ sig
   val zip : evar_map -> constr * t -> constr
   val check_native_args : CPrimitives.t -> t -> bool
   val get_next_primitive_args : CPrimitives.args_red -> t -> CPrimitives.args_red * (t * EConstr.t * t) option
-  val expand_case : env -> evar_map -> case_stk -> case_info * EInstance.t * constr array * (rel_context * constr) * (rel_context * constr) array
+  val expand_case : env -> evar_map -> case_stk -> case_info * EInstance.t * constr array * ((rel_context * constr) * Sorts.relevance) * (rel_context * constr) array
 end =
 struct
   open EConstr
@@ -312,7 +312,7 @@ struct
         let t1,l1 = decomp_node_last n1 q1 in
         let t2,l2 = decomp_node_last n2 q2 in
         aux (f o t1 t2) l1 l2
-      | Case ((_,_,pms1,(_, t1),_,a1)) :: q1, Case ((_,_,pms2, (_, t2),_,a2)) :: q2 ->
+      | Case ((_,_,pms1,((_, t1),_),_,a1)) :: q1, Case ((_,_,pms2, ((_, t2),_),_,a2)) :: q2 ->
         let f' o (_, t1) (_, t2) = f o t1 t2 in
         aux (Array.fold_left2 f' (f (Array.fold_left2 f o pms1 pms2) t1 t2) a1 a2) q1 q2
       | Proj (p1,_) :: q1, Proj (p2,_) :: q2 ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index aba76b78f646..b9f970edd6b9 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -114,7 +114,7 @@ module Stack : sig
   val zip : evar_map -> constr * t -> constr
 
   val expand_case : env -> evar_map -> case_stk ->
-    case_info * EInstance.t * constr array * (rel_context * constr) * (rel_context * constr) array
+    case_info * EInstance.t * constr array * ((rel_context * constr) * Sorts.relevance) * (rel_context * constr) array
 end
 
 (************************************************************************)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3814fd4617fa..32cc48fad68d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -152,7 +152,7 @@ let retype ?(polyprop=true) sigma =
     | Ind ind -> Inductiveops.e_type_of_inductive env sigma ind
     | Construct c -> Inductiveops.e_type_of_constructor env sigma c
     | Case (ci,u,pms,p,iv,c,lf) ->
-        let (_,p,iv,c,lf) = EConstr.expand_case env sigma (ci,u,pms,p,iv,c,lf) in
+        let (_,(p,_),iv,c,lf) = EConstr.expand_case env sigma (ci,u,pms,p,iv,c,lf) in
         let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
@@ -350,7 +350,7 @@ let relevance_of_term env sigma c =
       | Construct (c,u) ->
         let u = Unsafe.to_instance u in
         Relevanceops.relevance_of_constructor env (c,u)
-      | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
+      | Case (_, _, _, (_, r), _, _, _) -> r
       | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
       | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
       | Proj (p, r, _) -> r
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 57277d37b5c2..846672d6d0f0 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -218,7 +218,7 @@ let unify_relevance sigma r1 r2 =
     in
     Some sigma
 
-let judge_of_case env sigma case ci pj iv cj lfj =
+let judge_of_case env sigma case ci (pj,rp) iv cj lfj =
   let ((ind, u), spec) =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj in
@@ -226,16 +226,18 @@ let judge_of_case env sigma case ci pj iv cj lfj =
   let () = if Inductive.is_private specif then Type_errors.error_case_on_private_ind env ind in
   let indspec = ((ind, EInstance.kind sigma u), spec) in
   let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec specif pj cj.uj_val in
-  (* should we have evar map aware check_case_info and should_invert_case? *)
-  let sigma, ci =
-    if Sorts.relevance_equal ci.ci_relevance rci then sigma, ci
-    else match unify_relevance sigma ci.ci_relevance rci with
-    | None -> sigma, ci (* will fail in check_case_info *)
-    | Some sigma -> sigma, { ci with ci_relevance = rci }
+  (* should we have evar map aware should_invert_case? *)
+  let sigma, rp =
+    if Sorts.relevance_equal rp rci then sigma, rp
+    else match unify_relevance sigma rp rci with
+    | None ->
+      raise_type_error (env,sigma,Type_errors.BadCaseRelevance (rp, mkCase case))
+    | Some sigma -> sigma, rci
   in
-  let () = check_case_info env (fst indspec) rci ci in
+  let () = check_case_info env (fst indspec) ci in
   let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in
-  let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
+  let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true)
+              != should_invert_case env rp ci
     then Type_errors.error_bad_invert env
   in
   sigma, { uj_val  = mkCase case;
@@ -491,7 +493,7 @@ let rec execute env sigma cstr =
 
     | Case (ci, u, pms, p, iv, c, lf) ->
         let case = (ci, u, pms, p, iv, c, lf) in
-        let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in
+        let (ci, (p,rp), iv, c, lf) = EConstr.expand_case env sigma case in
         let sigma, cj = execute env sigma c in
         let sigma, pj = execute env sigma p in
         let sigma, lfj = execute_array env sigma lf in
@@ -505,7 +507,7 @@ let rec execute env sigma cstr =
             let sigma = check_actual_type env sigma cj tj.utj_val in
             sigma
         in
-        judge_of_case env sigma case ci pj iv cj lfj
+        judge_of_case env sigma case ci (pj,rp) iv cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
         let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
@@ -718,9 +720,9 @@ let rec recheck_against env sigma good c =
 
     | Case (gci, gu, gpms, gp, giv, gc, glf),
       Case (ci, u, pms, p, iv, c, lf) ->
-      let (gci, gp, giv, gc, glf) = EConstr.expand_case env sigma (gci, gu, gpms, gp, giv, gc, glf) in
+      let (gci, (gp,_), giv, gc, glf) = EConstr.expand_case env sigma (gci, gu, gpms, gp, giv, gc, glf) in
       let case = (ci, u, pms, p, iv, c, lf) in
-      let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in
+      let (ci, (p,rp), iv, c, lf) = EConstr.expand_case env sigma case in
       let sigma, changedc, cj = recheck_against env sigma gc c in
       let sigma, changedp, pj = recheck_against env sigma gp p in
       let (sigma, changedlf), lfj =
@@ -758,7 +760,7 @@ let rec recheck_against env sigma good c =
       in
       if unchanged changedc && unchanged changedp && unchanged changediv && bodyonly changedlf
       then assume_unchanged_type sigma
-      else maybe_changed (judge_of_case env sigma case ci pj iv cj lfj)
+      else maybe_changed (judge_of_case env sigma case ci (pj,rp) iv cj lfj)
 
     | Proj (gp, _, gc),
       Proj (p, _, c) ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 51fd685ad9b9..9f99ec489887 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -854,12 +854,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
                unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
              | _ -> raise ex)
 
-        | Case (ci1, u1, pms1, p1, iv1, c1, cl1), Case (ci2, u2, pms2, p2, iv2, c2, cl2) ->
+        | Case (ci1, u1, pms1, p1, iv1, c1, cl1), Case (ci2, u2, pms2, (p2,_), iv2, c2, cl2) ->
             (try
              let () = if not (QInd.equal curenv ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN) in
              let opt' = {opt with at_top = true; with_types = false} in
              let substn = Array.fold_left2 (unirec_rec curenvnb CONV ~nargs:0 opt') substn pms1 pms2 in
-             let (ci1, _, _, p1, _, c1, cl1) = EConstr.annotate_case env sigma (ci1, u1, pms1, p1, iv1, c1, cl1) in
+             let (ci1, _, _, (p1,_), _, c1, cl1) = EConstr.annotate_case env sigma (ci1, u1, pms1, p1, iv1, c1, cl1) in
              let unif opt substn (ctx1, c1) (_, c2) =
                let curenvnb' = List.fold_right (fun decl (env, n) -> push_rel decl env, n + 1) ctx1 curenvnb in
                unirec_rec curenvnb' CONV opt' substn c1 c2
@@ -1895,7 +1895,7 @@ let rec make sigma c0 = match EConstr.kind sigma c0 with
   (* Unification doesn't recurse on the subterms in evar instances *)
   let data = SList.Skip.fold (fun accu v -> max accu (get_max_rel sigma v)) 0 al in
   { proj = c0; self = AOther [||]; data }
-| Case (ci, u, pms, p, iv, c, bl) ->
+| Case (ci, u, pms, (p,_), iv, c, bl) ->
   let pmsd = get_max_rel_array sigma pms in
   let pd =
     let (nas, p) = p in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index cb476c43839e..6ec472c7a039 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -302,12 +302,12 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type (pctx, p) realargs c in
       let p = (get_case_annot pctx, p) in
-      let ci = Inductiveops.make_case_info env ind relevance RegularStyle in
-      let iv = if Typeops.should_invert_case env ci then
+      let ci = Inductiveops.make_case_info env ind RegularStyle in
+      let iv = if Typeops.should_invert_case env relevance ci then
           CaseInvert {indices=realargs}
         else NoInvert
       in
-      nf_stk env sigma (mkCase (ci, u, params, p, iv, c, branchs)) tcase stk
+      nf_stk env sigma (mkCase (ci, u, params, (p,relevance), iv, c, branchs)) tcase stk
   | Zproj p :: stk ->
     let () = assert (from = 0) in
     let ((ind, u), args) = Inductiveops.find_mrectype env sigma (EConstr.of_constr t) in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c675a7e274a4..55b45f8d262a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -828,17 +828,17 @@ let build_case_analysis env sigma (ind, u) params pred indices indarg dep knd =
 
   match projs with
   | None ->
-    let ci = make_case_info env ind relevance RegularStyle in
+    let ci = make_case_info env ind RegularStyle in
     let pbody =
       mkApp
         (pred,
           if dep then Context.Rel.instance mkRel 0 deparsign
           else Context.Rel.instance mkRel 1 (List.tl deparsign)) in
     let iv =
-      if Typeops.should_invert_case env ci then CaseInvert { indices = indices }
+      if Typeops.should_invert_case env relevance ci then CaseInvert { indices = indices }
       else NoInvert
     in
-    RealCase (ci, u, params, (pnas, pbody), iv, indarg)
+    RealCase (ci, u, params, ((pnas, pbody), relevance), iv, indarg)
   | Some ps ->
     let args = Array.map (fun (p,r) ->
         let r = UVars.subst_instance_relevance (Unsafe.to_instance u) r in
@@ -911,11 +911,11 @@ let case_pf ?(with_evars=false) ~dep (indarg, typ) =
   let rec nf_betaiota c = EConstr.map sigma nf_betaiota (whd_betaiota env sigma c) in
   (* Call the legacy refiner on the result *)
   let arg = match body with
-  | RealCase (ci, u, pms, p, iv, c) ->
+  | RealCase (ci, u, pms, (p,r), iv, c) ->
     let c = nf_betaiota c in
     let pms = Array.map nf_betaiota pms in
     let p = on_snd nf_betaiota p in
-    Internal.Case ((ci, u, pms, p, iv, c), branches)
+    Internal.Case ((ci, u, pms, (p,r), iv, c), branches)
   | PrimitiveEta args ->
     let mv = new_meta () in
     let (ctx, t) = branches.(0) in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 213992bf0661..cdb49fa910a4 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -185,7 +185,7 @@ struct
     | Construct (c,u)-> Some (DRef (ConstructRef c), [])
     | Meta _         -> assert false
     | Evar (i,_)     -> None
-    | Case (ci,u1,pms1,c1,_iv,c2,ca)     ->
+    | Case (ci,u1,pms1,(c1,_),_iv,c2,ca)     ->
       let f_ctx (_, p) = p in
       Some (DCase(ci), [f_ctx c1; c2] @ Array.map_to_list f_ctx ca)
     | Fix ((ia,i),(_,ta,ca)) ->
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 9d46dc0b8785..91c1b3c3019c 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -544,7 +544,7 @@ let debug_RAKAM = Reductionops.debug_RAKAM
 let equal_stacks sigma (x, l) (y, l') =
   let f_equal x y = eq_constr sigma x y in
   let eq_fix a b = f_equal (mkFix a) (mkFix b) in
-  let eq_case (ci1, u1, pms1, p1, _, br1) (ci2, u2, pms2, p2, _, br2) =
+  let eq_case (ci1, u1, pms1, (p1,_), _, br1) (ci2, u2, pms2, (p2,_), _, br2) =
     Array.equal f_equal pms1 pms2 &&
     f_equal (snd p1) (snd p2) &&
     Array.equal (fun (_, c1) (_, c2) -> f_equal c1 c2) br1 br2
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 2f67a5e4e791..d35b60e6b12b 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -211,21 +211,28 @@ let build_sym_scheme env _handle ind =
   let realsign_ind =
     name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
   let rci = Sorts.Relevant in (* TODO relevance *)
-  let ci = make_case_info env ind rci RegularStyle in
+  let ci = make_case_info env ind RegularStyle in
+  let p =
+    my_it_mkLambda_or_LetIn_name env
+      (lift_rel_context (nrealargs+1) realsign_ind)
+      (mkApp (mkIndU indu,
+              Array.concat
+                [Context.Rel.instance mkRel (3*nrealargs+2) paramsctxt1;
+                 rel_vect 1 nrealargs;
+                 rel_vect (2*nrealargs+2) nrealargs]))
+  in
   let c =
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name env realsign_ind
-  (mkCase (Inductive.contract_case env (ci,
-     my_it_mkLambda_or_LetIn_name env
-       (lift_rel_context (nrealargs+1) realsign_ind)
-       (mkApp (mkIndU indu,Array.concat
-          [Context.Rel.instance mkRel (3*nrealargs+2) paramsctxt1;
-           rel_vect 1 nrealargs;
-           rel_vect (2*nrealargs+2) nrealargs])),
-           NoInvert,
-     mkRel 1 (* varH *),
-       [|cstr (nrealargs+1)|])))))
-  in c, UState.of_context_set ctx
+     (mkCase
+        (Inductive.contract_case env
+           (ci,
+            (p,rci),
+            NoInvert,
+            mkRel 1 (* varH *),
+            [|cstr (nrealargs+1)|])))))
+  in
+  c, UState.of_context_set ctx
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
@@ -272,12 +279,12 @@ let build_sym_involutive_scheme env handle ind =
   let realsign_ind =
     name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
   let rci = Sorts.Relevant in (* TODO relevance *)
-  let ci = make_case_info env ind rci RegularStyle in
+  let ci = make_case_info env ind RegularStyle in
   let c =
     (my_it_mkLambda_or_LetIn paramsctxt
      (my_it_mkLambda_or_LetIn_name env realsign_ind
       (mkCase (Inductive.contract_case env (ci,
-                my_it_mkLambda_or_LetIn_name env
+                (my_it_mkLambda_or_LetIn_name env
                 (lift_rel_context (nrealargs+1) realsign_ind)
                 (mkApp (eq,[|
                 mkApp
@@ -294,7 +301,7 @@ let build_sym_involutive_scheme env handle ind =
                  rel_vect (2*nrealargs+2) nrealargs;
                  rel_vect 1 nrealargs;
                  [|mkRel 1|]])|]]);
-               mkRel 1|])),
+               mkRel 1|])), rci),
                NoInvert,
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
@@ -411,8 +418,8 @@ let build_l2r_rew_scheme dep env handle ind kind =
   let ctx = UnivGen.sort_context_union ctx ctx' in
   let s = mkSort s in
   let rci = Sorts.Relevant in (* TODO relevance *)
-  let ci = make_case_info env ind rci RegularStyle in
-  let cieq = make_case_info env (fst (destInd eq)) rci RegularStyle in
+  let ci = make_case_info env ind RegularStyle in
+  let cieq = make_case_info env (fst (destInd eq)) RegularStyle in
   let applied_PC =
     mkApp (mkVar varP,Array.append (Context.Rel.instance mkRel 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
@@ -434,7 +441,7 @@ let build_l2r_rew_scheme dep env handle ind kind =
                [|mkRel 2|]])|]]) in
   let main_body =
     mkCase (Inductive.contract_case env (ci,
-            my_it_mkLambda_or_LetIn_name env realsign_ind_G applied_PG,
+            (my_it_mkLambda_or_LetIn_name env realsign_ind_G applied_PG, rci),
             NoInvert,
             applied_sym_C 3,
             [|mkVar varHC|]))
@@ -448,10 +455,10 @@ let build_l2r_rew_scheme dep env handle ind kind =
   (mkNamedLambda (make_annot varH indr) (lift 2 applied_ind)
      (if dep then (* we need a coercion *)
      mkCase (Inductive.contract_case env (cieq,
-       mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
+       (mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
          mkLambda (make_annot Anonymous indr,
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
-                   applied_PR)),
+                   applied_PR)), rci),
        NoInvert,
        mkApp (sym_involutive,
          Array.append (Context.Rel.instance mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
@@ -519,7 +526,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let ctx = UnivGen.sort_context_union ctx ctx' in
   let s = mkSort s in
   let rci = Sorts.Relevant in
-  let ci = make_case_info env ind rci RegularStyle in
+  let ci = make_case_info env ind RegularStyle in
   let applied_PC =
     mkApp (mkVar varP,Array.append
            (rel_vect (nrealargs*2+3) nrealargs)
@@ -537,12 +544,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   (my_it_mkLambda_or_LetIn_name env realsign
   (mkNamedLambda (make_annot varH indr) applied_ind
   (mkCase (Inductive.contract_case env (ci,
-     my_it_mkLambda_or_LetIn_name env
+     (my_it_mkLambda_or_LetIn_name env
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkNamedProd (make_annot varP indr)
          (my_it_mkProd_or_LetIn
            (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s)
-       (mkNamedProd (make_annot varHC indr) applied_PC applied_PG)),
+       (mkNamedProd (make_annot varHC indr) applied_PC applied_PG)), rci),
      NoInvert,
      (mkVar varH),
      [|mkNamedLambda (make_annot varP indr)
@@ -601,7 +608,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let ctx = UnivGen.sort_context_union ctx ctx' in
   let s = mkSort s in
   let rci = Sorts.Relevant in (* TODO relevance *)
-  let ci = make_case_info env ind rci RegularStyle in
+  let ci = make_case_info env ind RegularStyle in
   let applied_PC =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
@@ -617,9 +624,9 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   (mkNamedLambda (make_annot varHC indr) (lift 1 applied_PG)
   (mkApp
     (mkCase (Inductive.contract_case env (ci,
-       my_it_mkLambda_or_LetIn_name env
+       (my_it_mkLambda_or_LetIn_name env
          (lift_rel_context (nrealargs+3) realsign_ind)
-         (mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)),
+         (mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)), rci),
        NoInvert,
        mkRel 3 (* varH *),
        [|mkLambda
@@ -808,7 +815,7 @@ let build_congr env (eq,refl,ctx) ind =
   let varH,avoid = fresh env (Id.of_string "H") avoid in
   let varf,avoid = fresh env (Id.of_string "f") avoid in
   let rci = Sorts.Relevant in (* TODO relevance *)
-  let ci = make_case_info env ind rci RegularStyle in
+  let ci = make_case_info env ind RegularStyle in
   let uni, ctx' = UnivGen.new_global_univ () in
   let ctx =
     let (qs,us),csts = ctx in
@@ -825,7 +832,7 @@ let build_congr env (eq,refl,ctx) ind =
             Context.Rel.instance_list mkRel (mip.mind_nrealargs+2) paramsctxt @
             Context.Rel.instance_list mkRel 0 realsign))
      (mkCase (Inductive.contract_case env (ci,
-       my_it_mkLambda_or_LetIn_name env
+       (my_it_mkLambda_or_LetIn_name env
          (lift_rel_context (mip.mind_nrealargs+3) realsign)
          (mkLambda
            (make_annot Anonymous Sorts.Relevant,
@@ -837,7 +844,7 @@ let build_congr env (eq,refl,ctx) ind =
             mkApp (eq,
               [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
-                mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
+                mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), rci),
        NoInvert,
        mkVar varH,
        [|mkApp (refl,
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9b5807ab2e94..cfcab8225741 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -909,8 +909,8 @@ let descend_then env sigma head dirn =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let rci = Sorts.Relevant in (* TODO relevance *)
-      let ci = make_case_info env ind rci RegularStyle in
-      Inductiveops.make_case_or_project env sigma indt ci p head (Array.of_list brl)))
+      let ci = make_case_info env ind RegularStyle in
+      Inductiveops.make_case_or_project env sigma indt ci (p, rci) head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -955,8 +955,8 @@ let build_selector env sigma dirn c ind special default =
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let rci = Sorts.Relevant in (* TODO relevance *)
-  let ci = make_case_info env ind rci RegularStyle in
-  let ans = Inductiveops.make_case_or_project env sigma indt ci p c (Array.of_list brl) in
+  let ci = make_case_info env ind RegularStyle in
+  let ans = Inductiveops.make_case_or_project env sigma indt ci (p, rci) c (Array.of_list brl) in
   ans
 
 let build_coq_False () = pf_constr_of_global (lib_ref "core.False.type")
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 7a1a2d133fc6..25922e7f17ce 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -931,7 +931,7 @@ let make_leibniz_proof env c ty r =
 
 let fold_match ?(force=false) env sigma c =
   let case = destCase sigma c in
-  let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in
+  let (ci, (p,_), iv, c, brs) = EConstr.expand_case env sigma case in
   let cty = Retyping.get_type_of env sigma c in
   let dep, pred, sk =
     let env', ctx, body =
@@ -1171,7 +1171,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
         in state, res
 
       | Case (ci, u, pms, p, iv, c, brs) ->
-        let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
+        let (ci, (p,rp), iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
         let cty = Retyping.get_type_of env (goalevars evars) c in
         let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
         let cstr' = Some eqty in
@@ -1181,7 +1181,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
         let state, res =
           match c' with
           | Success r ->
-            let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in
+            let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, (lift 1 p,rp), map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in
             let res = make_leibniz_proof env case ty r in
               state, Success (coerce env (prop,cstr) res)
           | Fail | Identity ->
@@ -1203,7 +1203,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
               in
                 match found with
                 | Some r ->
-                  let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
+                  let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, (lift 1 p, rp), map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
                     state, Success (make_leibniz_proof env ctxc ty r)
                 | None -> state, c'
             else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index eac1de09980c..dc964ea23bc8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1704,12 +1704,12 @@ let make_projection env sigma params cstr sign elim i n c (ind, u) =
         if Sorts.family_leq ksort mip.mind_kelim then
           let arity = List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt in
           let mknas ctx = Array.of_list (List.rev_map get_annot ctx) in
-          let ci = Inductiveops.make_case_info env ind (get_relevance decl) RegularStyle in
+          let ci = Inductiveops.make_case_info env ind RegularStyle in
           let br = [| mknas cs_args, b |] in
           let args = Context.Rel.instance mkRel 0 sign in
           let pnas = Array.append (mknas arity) [|make_annot Anonymous mip.mind_relevance|] in
           let p = (pnas, lift (Array.length pnas) t) in
-          let c = mkCase (ci, u, Array.of_list params, p, NoInvert, mkApp (c, args), br) in
+          let c = mkCase (ci, u, Array.of_list params, (p, get_relevance decl), NoInvert, mkApp (c, args), br) in
           Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
         else None
       else
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 9f148b8a72fb..ab0c6a81cea9 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -62,7 +62,7 @@ Ltac2 Type kind := [
 | Constant (constant, instance)
 | Ind (inductive, instance)
 | Constructor (constructor, instance)
-| Case (case, constr, case_invert, constr, constr array)
+| Case (case, (constr * Binder.relevance), case_invert, constr, constr array)
 | Fix (int array, int, binder array, constr array)
 | CoFix (int, binder array, constr array)
 | Proj (projection, Binder.relevance, constr)
@@ -116,7 +116,7 @@ Ltac2 constructor (ind : inductive) (i : int) : constructor :=
 
 Module Case.
   Ltac2 @ external equal : case -> case -> bool := "coq-core.plugins.ltac2" "constr_case_equal".
-  (** Checks equality of the inductive and relevance components of the
+  (** Checks equality of the inductive components of the
       case info. When comparing the inductives, those obtained through
       module aliases or Include are not considered equal by this
       function. *)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 5189289dc855..24158e38ae6f 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -183,7 +183,7 @@ let fold_with_full_binders g f n acc c =
   | Evar _ -> assert false
   | Case (ci, u, pms, p, iv, c, bl) ->
     let mib = lookup_mind (fst ci.ci_ind) in
-    let (ci, p, iv, c, bl) = Inductive.expand_case_specif mib (ci, u, pms, p, iv, c, bl) in
+    let (ci, (p,_), iv, c, bl) = Inductive.expand_case_specif mib (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
@@ -221,7 +221,7 @@ let rec traverse current ctx accu t =
 | Construct (((mind, _), _) as cst, _) ->
   traverse_inductive accu mind (ConstructRef cst)
 | Meta _ | Evar _ -> assert false
-| Case (_, _, _, ([|_|], oty), _, c, [||]) when Vars.noccurn 1 oty ->
+| Case (_, _, _, (([|_|], oty),_), _, c, [||]) when Vars.noccurn 1 oty ->
     (* non dependent match on an inductive with no constructors *)
     begin match Constr.kind c with
     | Const (kn, _) when not (Declareops.constant_has_body (lookup_constant kn)) ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 55baba62ec0e..2e57bbb8b527 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -438,12 +438,12 @@ let build_beq_scheme env handle kn =
     (* The restricted translation translates only types *)
     | Lambda _ | Construct _ -> assert false
 
-    | Case (ci, u, pms, (pnames,p), iv, tm, lbr) ->
+    | Case (ci, u, pms, ((pnames,p),r), iv, tm, lbr) ->
       let env_lift_pred = shiftn_env_lift (Array.length pnames) env_lift in
       let t =
         mkCase (ci, u,
           Array.map (translate_term env_lift_pred) pms,
-          translate_term_with_binders env_lift_pred (pnames,p),
+          (translate_term_with_binders env_lift_pred (pnames,p), r),
           Constr.map_invert (translate_term env_lift_pred) iv,
           mkRel 1,
           Array.map (translate_term_with_binders env_lift_pred) lbr) in
@@ -458,7 +458,7 @@ let build_beq_scheme env handle kn =
         | Some t_eq -> Some (names, mkLambda (na, t, t_eq))) lbr in
       if Array.for_all Option.has_some lbr then
         let lbr = Array.map Option.get lbr in
-        let case = mkCase (ci, u, pms, (pnames, p), iv, translate_term env_lift tm, lbr) in
+        let case = mkCase (ci, u, pms, ((pnames, p), r), iv, translate_term env_lift tm, lbr) in
         Some (mkApp (case, [|c|]))
       else
         None
@@ -550,14 +550,14 @@ let build_beq_scheme env handle kn =
        translate_type_eq, preserve the types in Construct/CoFix *)
     | Proj _ | Construct _ | CoFix _ -> None
 
-    | Case (ci, u, pms, (pnames,p), iv, tm, lbr) ->
+    | Case (ci, u, pms, ((pnames,p), r), iv, tm, lbr) ->
       let pctx = pred_context env ci pms u pnames in
       let env_lift_pred = List.fold_right push_env_lift pctx env_lift in
       let n = Array.length pnames in
       let c =
         mkCase (ci, u,
           Array.map (lift n) pms,
-          (pnames, liftn n (n+1) p),
+          ((pnames, liftn n (n+1) p), r),
           Constr.map_invert (lift n) iv,
           mkRel 1,
           Array.map (fun (names, br) -> (names, let q = Array.length names in liftn n (n+q+1) br)) lbr) in
@@ -570,7 +570,7 @@ let build_beq_scheme env handle kn =
         | Some t_eq -> Some (names, t_eq)) lbr in
       if Array.for_all Option.has_some lbr && Option.has_some p then
         let lbr = Array.map Option.get lbr in
-        Some (mkCase (ci, u, pms, (pnames, Option.get p), iv, translate_term env_lift tm, lbr))
+        Some (mkCase (ci, u, pms, ((pnames, Option.get p), r), iv, translate_term env_lift tm, lbr))
       else
         None
 
@@ -773,7 +773,7 @@ let build_beq_scheme env handle kn =
         make_andb_list eqs
       | None ->
         (* An inductive type *)
-        let ci = make_case_info env ind rci MatchStyle in
+        let ci = make_case_info env ind MatchStyle in
         let nconstr = Array.length constrs in
         let ar =
           Array.init nconstr (fun i ->
@@ -810,7 +810,7 @@ let build_beq_scheme env handle kn =
           let predj = EConstr.of_constr (translate_term env_lift_recparams_fix_nonrecparams_tomatch_csargsi pred) in
           let case =
             simple_make_case_or_project env (Evd.from_env env)
-              ci predj NoInvert (EConstr.mkRel (nb_cstr_args + 1))
+              ci (predj,rci) NoInvert (EConstr.mkRel (nb_cstr_args + 1))
               (EConstr.of_constr_array ar2)
           in
           let cs_argsi = translate_context env_lift_recparams_fix_nonrecparams_tomatch constrs.(i).cs_args in
@@ -819,7 +819,7 @@ let build_beq_scheme env handle kn =
         let predi = EConstr.of_constr (translate_term env_lift_recparams_fix_nonrecparams_tomatch pred) in
         let case =
           simple_make_case_or_project env (Evd.from_env env)
-            ci predi NoInvert (EConstr.mkRel 2)
+            ci (predi,rci) NoInvert (EConstr.mkRel 2)
             (EConstr.of_constr_array ar) in
         EConstr.Unsafe.to_constr case
     in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d3c2717986d7..5f34b0a265ad 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -820,9 +820,9 @@ let explain_bad_binder_relevance env sigma rlv decl =
     spc () ++ str "(maybe a bugged tactic)."
 
 let explain_bad_case_relevance env sigma rlv case =
-  let (ci, _, _, _, _, _, _) = EConstr.destCase sigma case in
+  let (_, _, _, (_,badr), _, _, _) = EConstr.destCase sigma case in
   strbrk "Pattern-matching" ++ spc () ++ pr_leconstr_env env sigma case ++
-    strbrk " has relevance mark set to " ++ pr_relevance sigma ci.ci_relevance ++
+    strbrk " has relevance mark set to " ++ pr_relevance sigma badr ++
     strbrk " but was expected to be " ++ pr_relevance sigma rlv ++
     spc () ++ str "(maybe a bugged tactic)."
 
diff --git a/vernac/record.ml b/vernac/record.ml
index a052dc2e7fcf..f0cb29feb7b0 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -400,10 +400,10 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
         let ccl' = liftn 1 2 ccl in
         let p = mkLambda (x, lift 1 rp, ccl') in
         let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
-        let ci = Inductiveops.make_case_info env indsp rci LetStyle in
+        let ci = Inductiveops.make_case_info env indsp LetStyle in
         (* Record projections are always NoInvert because they're at
            constant relevance *)
-        mkCase (Inductive.contract_case env (ci, p, NoInvert, mkRel 1, [|branch|])), None
+        mkCase (Inductive.contract_case env (ci, (p, rci), NoInvert, mkRel 1, [|branch|])), None
   in
   let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
   let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in