Merge PR #10390: UIP in SProp

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes

23 files changed, 413 insertions, 130 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index de02882370..9640efd8eb 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -343,6 +343,7 @@ and fterm =
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
+  | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs
   | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
   | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
@@ -353,6 +354,8 @@ and fterm =
   | FCLOS of constr * fconstr subs
   | FLOCKED
 
+and finvert = Univ.Instance.t * fconstr array
+
 let fterm_of v = v.term
 let set_norm v = v.mark <- Mark.set_norm v.mark
 let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false
@@ -375,16 +378,30 @@ type infos_cache = {
   i_env : env;
   i_sigma : existential -> constr option;
   i_share : bool;
+  i_univs : UGraph.t;
 }
 
 type clos_infos = {
   i_flags : reds;
+  i_relevances : Sorts.relevance Range.t;
   i_cache : infos_cache }
 
 type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t
 
 let info_flags info = info.i_flags
 let info_env info = info.i_cache.i_env
+let info_univs info = info.i_cache.i_univs
+
+let push_relevance infos r =
+  { infos with i_relevances = Range.cons r.Context.binder_relevance infos.i_relevances }
+
+let push_relevances infos nas =
+  { infos with i_relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l)
+                   infos.i_relevances nas }
+
+let set_info_relevances info r = { info with i_relevances = r }
+
+let info_relevances info = info.i_relevances
 
 (**********************************************************************)
 (* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *)
@@ -438,7 +455,7 @@ let rec lft_fconstr n ft =
       {mark=mark Cstr r; term=FCoFix(cfx,subs_shft(n,e))}
     | FLIFT(k,m) -> lft_fconstr (n+k) m
     | FLOCKED -> assert false
-    | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _
+    | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FCaseInvert _ | FProd _
       | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)}
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
@@ -558,14 +575,10 @@ let rec to_constr lfts v =
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
-    | FCaseT (ci,p,c,ve,env) ->
-      if is_subs_id env && is_lift_id lfts then
-        mkCase (ci, p, to_constr lfts c, ve)
-      else
-        let subs = comp_subs lfts env in
-        mkCase (ci, subst_constr subs p,
-            to_constr lfts c,
-            Array.map (fun b -> subst_constr subs b) ve)
+    | FCaseT (ci,p,c,ve,env) -> to_constr_case lfts ci p NoInvert c ve env
+    | FCaseInvert (ci,p,(univs,args),c,ve,env) ->
+      let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in
+       to_constr_case lfts ci p iv c ve env
     | FFix ((op,(lna,tys,bds)) as fx, e) ->
       if is_subs_id e && is_lift_id lfts then
         mkFix fx
@@ -628,6 +641,15 @@ let rec to_constr lfts v =
         subst_constr subs t
     | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
 
+and to_constr_case lfts ci p iv c ve env =
+  if is_subs_id env && is_lift_id lfts then
+    mkCase (ci, p, iv, to_constr lfts c, ve)
+  else
+    let subs = comp_subs lfts env in
+    mkCase (ci, subst_constr subs p, iv,
+            to_constr lfts c,
+            Array.map (fun b -> subst_constr subs b) ve)
+
 and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with
 | Rel i ->
   begin match expand_rel i subst with
@@ -931,7 +953,7 @@ let rec knh info m stk =
        | Some s -> knh info c (s :: zupdate info m stk))
 
 (* cases where knh stops *)
-    | (FFlex _|FLetIn _|FConstruct _|FEvar _|
+    | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _|
        FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) ->
         (m, stk)
 
@@ -940,8 +962,11 @@ 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,p,t,br) ->
+    | Case(ci,p,NoInvert,t,br) ->
         knht info e t (ZcaseT(ci, p, br, e)::stk)
+    | Case(ci,p,CaseInvert{univs;args},t,br) ->
+      let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
+      { mark = mark Red Unknown; term }, stk
     | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
     | Cast(a,_,_) -> knht info e a stk
     | Rel n -> knh info (clos_rel e n) stk
@@ -1250,6 +1275,10 @@ module FredNative = RedNative(FNativeEntries)
 
 (************************************************************************)
 
+let conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) ref
+  = ref (fun _ _ _ _ -> (assert false : bool))
+let set_conv f = conv := f
+
 (* Computes a weak head normal form from the result of knh. *)
 let rec knr info tab m stk =
   match m.term with
@@ -1325,8 +1354,13 @@ let rec knr info tab m stk =
            kni info tab a (Zprimitive(op,c,rargs,nargs)::s)
              end
      | (_, _, s) -> (m, s))
+  | FCaseInvert (ci,_p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
+    begin match case_inversion info tab ci iv v with
+      | Some c -> knit info tab env c stk
+      | None -> (m, stk)
+    end
   | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _
-    | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
+    | FFix _ | FCoFix _ | FCaseT _ | FCaseInvert _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
     | FCLOS _ -> (m, stk)
 
 
@@ -1338,6 +1372,28 @@ and knit info tab e t stk =
   let (ht,s) = knht info e t stk in
   knr info tab ht s
 
+and case_inversion info tab ci (univs,args) v =
+  let open Declarations in
+  if Array.is_empty args then Some v.(0)
+  else
+    let env = info_env info in
+    let ind = ci.ci_ind in
+    let params, indices = Array.chop ci.ci_npar args in
+    let psubst = subs_cons (params, subs_id 0) in
+    let mib = Environ.lookup_mind (fst ind) env in
+    let mip = mib.mind_packets.(snd ind) in
+    (* indtyping enforces 1 ctor with no letins in the context *)
+    let _, expect = mip.mind_nf_lc.(0) in
+    let _ind, expect_args = destApp expect in
+    let check_index i index =
+      let expected = expect_args.(ci.ci_npar + i) in
+      let expected = Vars.subst_instance_constr univs expected in
+      let expected = mk_clos psubst expected in
+      !conv {info with i_flags=all} tab expected index
+    in
+    if Array.for_all_i check_index 0 indices
+    then Some v.(0) else None
+
 let kh info tab v stk = fapp_stack(kni info tab v stk)
 
 (************************************************************************)
@@ -1348,7 +1404,7 @@ let rec zip_term zfun m stk =
     | Zapp args :: s ->
         zip_term zfun (mkApp(m, Array.map zfun args)) s
     | ZcaseT(ci,p,br,e)::s ->
-        let t = mkCase(ci, zfun (mk_clos e p), m,
+        let t = mkCase(ci, zfun (mk_clos e p), NoInvert, m,
                        Array.map (fun b -> zfun (mk_clos e b)) br) in
         zip_term zfun t s
     | Zproj p::s ->
@@ -1388,31 +1444,34 @@ and norm_head info tab m =
       | FLambda(_n,tys,f,e) ->
         let (e',info,rvtys) =
           List.fold_left (fun (e,info,ctxt) (na,ty) ->
+              let info = push_relevance info na in
               (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt))
             (e,info,[]) tys in
         let bd = kl info tab (mk_clos e' f) in
         List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
       | FLetIn(na,a,b,f,e) ->
           let c = mk_clos (subs_lift e) f in
-          mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
+          mkLetIn(na, kl info tab a, kl info tab b, kl (push_relevance info na) tab c)
       | FProd(na,dom,rng,e) ->
-          mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng))
+          mkProd(na, kl info tab dom, kl (push_relevance info na) tab (mk_clos (subs_lift e) rng))
       | FCoFix((n,(na,tys,bds)),e) ->
           let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
             Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
-          mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
+          let infobd = push_relevances info na in
+          mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl infobd tab) fbds))
       | FFix((n,(na,tys,bds)),e) ->
           let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
             Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
-          mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
+          let infobd = push_relevances info na in
+          mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl infobd tab) fbds))
       | FEvar((i,args),env) ->
           mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args)
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
-        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m
+      | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
 
@@ -1434,14 +1493,16 @@ let whd_stack infos tab m stk = match Mark.red_state m.mark with
   let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
   k
 
-let create_clos_infos ?(evars=fun _ -> None) flgs env =
+let create_clos_infos ?univs ?(evars=fun _ -> None) flgs env =
+  let univs = Option.default (universes env) univs in
   let share = (Environ.typing_flags env).Declarations.share_reduction in
   let cache = {
     i_env = env;
     i_sigma = evars;
     i_share = share;
+    i_univs = univs;
   } in
-  { i_flags = flgs; i_cache = cache }
+  { i_flags = flgs; i_relevances = Range.empty; i_cache = cache }
 
 let create_tab () = KeyTable.create 17
 
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 79092813bc..c1e5f12df7 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -95,10 +95,11 @@ module KeyTable : Hashtbl.S with type key = table_key
 (** [fconstr] is the type of frozen constr *)
 
 type fconstr
-
 (** [fconstr] can be accessed by using the function [fterm_of] and by
    matching on type [fterm] *)
 
+type finvert
+
 type fterm =
   | FRel of int
   | FAtom of constr (** Metas and Sorts *)
@@ -110,6 +111,7 @@ type fterm =
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
+  | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs
   | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
   | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
@@ -173,15 +175,22 @@ val set_relevance : Sorts.relevance -> fconstr -> unit
 type clos_infos
 type clos_tab
 val create_clos_infos :
-  ?evars:(existential->constr option) -> reds -> env -> clos_infos
+  ?univs:UGraph.t -> ?evars:(existential->constr option) -> reds -> env -> clos_infos
 val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
 val create_tab : unit -> clos_tab
 
 val info_env : clos_infos -> env
 val info_flags: clos_infos -> reds
+val info_univs : clos_infos -> UGraph.t
 val unfold_projection : clos_infos -> Projection.t -> stack_member option
 
+val push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos
+val push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos
+val set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos
+
+val info_relevances : clos_infos -> Sorts.relevance Range.t
+
 val infos_with_reds : clos_infos -> reds -> clos_infos
 
 (** Reduction function *)
@@ -214,6 +223,9 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** [unfold_reference] unfolds references in a [fconstr] *)
 val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def
 
+(** Hook for Reduction *)
+val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit
+
 (***********************************************************************
   i This is for lazy debug *)
 
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 65de52c0f6..0d77cae077 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -710,7 +710,7 @@ let rec lambda_of_constr env c =
 
   | Construct _ ->  lambda_of_app env c empty_args
 
-  | Case(ci,t,a,branches) ->
+  | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
     let ind = ci.ci_ind in
     let mib = lookup_mind (fst ind) env.global_env in
     let oib = mib.mind_packets.(snd ind) in
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 703e3616a0..d0598bdad1 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -83,6 +83,10 @@ type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
+type ('constr, 'univs) case_invert =
+  | NoInvert
+  | CaseInvert of { univs : 'univs; args : 'constr array }
+
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
 type ('constr, 'types, 'sort, 'univs) kind_of_term =
@@ -99,7 +103,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
-  | Case      of case_info * 'constr * 'constr * 'constr array
+  | Case      of case_info * 'constr * ('constr, 'univs) case_invert * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -189,7 +193,7 @@ let mkConstructU c = Construct c
 let mkConstructUi ((ind,u),i) = Construct ((ind,i),u)
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkCase (ci, p, c, ac) = Case (ci, p, c, ac)
+let mkCase (ci, p, iv, c, ac) = Case (ci, p, iv, c, ac)
 
 (* If recindxs = [|i1,...in|]
       funnames = [|f1,...fn|]
@@ -417,7 +421,7 @@ let destConstruct c = match kind c with
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind c with
-  | Case (ci,p,c,v) -> (ci,p,c,v)
+  | Case (ci,p,iv,c,v) -> (ci,p,iv,c,v)
   | _ -> raise DestKO
 
 let destProj c = match kind c with
@@ -461,6 +465,11 @@ let decompose_appvect c =
    starting from [acc] and proceeding from left to right according to
    the usual representation of the constructions; it is not recursive *)
 
+let fold_invert f acc = function
+  | NoInvert -> acc
+  | CaseInvert {univs=_;args} ->
+    Array.fold_left f acc args
+
 let fold f acc c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> acc
@@ -471,7 +480,7 @@ let fold f acc c = match kind c with
   | App (c,l) -> Array.fold_left f (f acc c) l
   | Proj (_p,c) -> f acc c
   | Evar (_,l) -> List.fold_left f acc l
-  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+  | Case (_,p,iv,c,bl) -> Array.fold_left f (f (fold_invert f (f acc p) iv) c) bl
   | Fix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
   | CoFix (_,(_lna,tl,bl)) ->
@@ -481,6 +490,11 @@ let fold f acc c = match kind c with
    not recursive and the order with which subterms are processed is
    not specified *)
 
+let iter_invert f = function
+  | NoInvert -> ()
+  | CaseInvert {univs=_; args;} ->
+    Array.iter f args
+
 let iter f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> ()
@@ -491,7 +505,7 @@ let iter f c = match kind c with
   | App (c,l) -> f c; Array.iter f l
   | Proj (_p,c) -> f c
   | Evar (_,l) -> List.iter f l
-  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
+  | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
 
@@ -510,7 +524,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) -> List.iter (fun c -> f n c) l
-  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
+  | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
   | Proj (_p,c) -> f n c
   | Fix (_,(_,tl,bl)) ->
       Array.Fun1.iter f n tl;
@@ -537,7 +551,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,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
   | Fix (_,(_,tl,bl)) ->
       let n' = iterate g (Array.length tl) n in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -623,6 +637,13 @@ let map_branches_with_full_binders g f l ci bl =
 let map_return_predicate_with_full_binders g f l ci p =
   map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p
 
+let map_invert f = function
+  | NoInvert -> NoInvert
+  | CaseInvert {univs;args;} as orig ->
+    let args' = Array.Smart.map f args in
+    if args == args' then orig
+    else CaseInvert {univs;args=args';}
+
 let map_gen userview f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> c
@@ -660,18 +681,20 @@ let map_gen userview f c = match kind c with
       let l' = List.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
-  | Case (ci,p,b,bl) when userview ->
+  | Case (ci,p,iv,b,bl) when userview ->
       let b' = f b in
+      let iv' = map_invert f iv in
       let p' = map_return_predicate f ci p in
       let bl' = map_branches f ci bl in
-      if b'==b && p'==p && bl'==bl then c
-      else mkCase (ci, p', b', bl')
-  | Case (ci,p,b,bl) ->
+      if b'==b && iv'==iv && p'==p && bl'==bl then c
+      else mkCase (ci, p', iv', b', bl')
+  | Case (ci,p,iv,b,bl) ->
       let b' = f b in
+      let iv' = map_invert f iv in
       let p' = f p in
       let bl' = Array.Smart.map f bl in
-      if b'==b && p'==p && bl'==bl then c
-      else mkCase (ci, p', b', bl')
+      if b'==b && iv'==iv && p'==p && bl'==bl then c
+      else mkCase (ci, p', iv', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.Smart.map f tl in
       let bl' = Array.Smart.map f bl in
@@ -688,6 +711,13 @@ let map = map_gen false
 
 (* Like {!map} but with an accumulator. *)
 
+let fold_map_invert f acc = function
+  | NoInvert -> acc, NoInvert
+  | CaseInvert {univs;args;} as orig ->
+    let acc, args' = Array.fold_left_map f acc args in
+    if args==args' then acc, orig
+    else acc, CaseInvert {univs;args=args';}
+
 let fold_map f accu c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> accu, c
@@ -726,12 +756,13 @@ let fold_map f accu c = match kind c with
       let accu, l' = List.fold_left_map f accu l in
       if l'==l then accu, c
       else accu, mkEvar (e, l')
-  | Case (ci,p,b,bl) ->
+  | Case (ci,p,iv,b,bl) ->
       let accu, b' = f accu b in
+      let accu, iv' = fold_map_invert f accu iv in
       let accu, p' = f accu p in
       let accu, bl' = Array.Smart.fold_left_map f accu bl in
-      if b'==b && p'==p && bl'==bl then accu, c
-      else accu, mkCase (ci, p', b', bl')
+      if b'==b && iv'==iv && p'==p && bl'==bl then accu, c
+      else accu, mkCase (ci, p', iv', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
       let accu, tl' = Array.Smart.fold_left_map f accu tl in
       let accu, bl' = Array.Smart.fold_left_map f accu bl in
@@ -786,12 +817,13 @@ let map_with_binders g f l c0 = match kind c0 with
     let al' = List.Smart.map (fun c -> f l c) al in
     if al' == al then c0
     else mkEvar (e, al')
-  | Case (ci, p, c, bl) ->
+  | Case (ci, p, iv, c, bl) ->
     let p' = f l p in
+    let iv' = map_invert (f l) iv in
     let c' = f l c in
     let bl' = Array.Fun1.Smart.map f l bl in
-    if p' == p && c' == c && bl' == bl then c0
-    else mkCase (ci, p', c', bl')
+    if p' == p && iv' == iv && c' == c && bl' == bl then c0
+    else mkCase (ci, p', iv', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
     let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
@@ -836,7 +868,7 @@ let fold_with_full_binders g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -847,7 +879,7 @@ let fold_with_full_binders g f n acc c =
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
 
-type 'univs instance_compare_fn = GlobRef.t -> int ->
+type 'univs instance_compare_fn = (GlobRef.t * int) option ->
   'univs -> 'univs -> bool
 
 type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
@@ -863,6 +895,14 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
+let eq_invert eq leq_universes iv1 iv2 =
+  match iv1, iv2 with
+  | NoInvert, NoInvert -> true
+  | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
+  | CaseInvert {univs;args}, CaseInvert iv2 ->
+    leq_universes univs iv2.univs
+    && Array.equal eq args iv2.args
+
 let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 =
   match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with
   | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *)
@@ -884,12 +924,12 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
-    Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2
+    Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2
+  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
   | Construct (c1,u1), Construct (c2,u2) ->
-    eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2
-  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-    eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
+    eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
+  | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
+    eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
     Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
     && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
@@ -923,7 +963,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
 let compare_head_gen eq_universes eq_sorts eq t1 t2 =
   compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
 
-let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal
+let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
 
 (*******************************)
 (*  alpha conversion functions *)
@@ -932,14 +972,14 @@ let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal
 (* alpha conversion : ignore print names and casts *)
 
 let rec eq_constr nargs m n =
-  (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n
+  (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr nargs m n
 
 let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *)
 
 let eq_constr_univs univs m n =
   if m == n then true
   else
-    let eq_universes _ _ = UGraph.check_eq_instances univs in
+    let eq_universes _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let rec eq_constr' nargs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
@@ -948,7 +988,7 @@ let eq_constr_univs univs m n =
 let leq_constr_univs univs m n =
   if m == n then true
   else
-    let eq_universes _ _ = UGraph.check_eq_instances univs in
+    let eq_universes _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = s1 == s2 ||
       UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let leq_sorts s1 s2 = s1 == s2 ||
@@ -965,7 +1005,7 @@ let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
   else
     let cstrs = ref Constraint.empty in
-    let eq_universes _ _ = UGraph.check_eq_instances univs in
+    let eq_universes _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
@@ -985,7 +1025,7 @@ let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
   else
     let cstrs = ref Constraint.empty in
-    let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in
+    let eq_universes _ l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
@@ -1015,7 +1055,16 @@ let leq_constr_univs_infer univs m n =
     res, !cstrs
 
 let rec eq_constr_nounivs m n =
-  (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n
+  (m == n) || compare_head_gen (fun _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n
+
+let compare_invert f iv1 iv2 =
+  match iv1, iv2 with
+  | NoInvert, NoInvert -> 0
+  | NoInvert, CaseInvert _ -> -1
+  | CaseInvert _, NoInvert -> 1
+  | CaseInvert iv1, CaseInvert iv2 ->
+    (* univs ignored deliberately *)
+    Array.compare f iv1.args iv2.args
 
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
@@ -1060,8 +1109,12 @@ let constr_ord_int f t1 t2 =
     | Ind _, _ -> -1 | _, Ind _ -> 1
     | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2
     | Construct _, _ -> -1 | _, Construct _ -> 1
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-        ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
+    | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
+      let c = f p1 p2 in
+      if Int.equal c 0 then let c = compare_invert f iv1 iv2 in
+      if Int.equal c 0 then let c = f c1 c2 in
+      if Int.equal c 0 then Array.compare f bl1 bl2
+      else c else c else c
     | Case _, _ -> -1 | _, Case _ -> 1
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
         ((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
@@ -1129,6 +1182,14 @@ let array_eqeq t1 t2 =
      (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
    in aux 0)
 
+let invert_eqeq iv1 iv2 =
+  match iv1, iv2 with
+  | NoInvert, NoInvert -> true
+  | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
+  | CaseInvert iv1, CaseInvert iv2 ->
+    iv1.univs == iv2.univs
+    && iv1.args == iv2.args
+
 let hasheq t1 t2 =
   match t1, t2 with
     | Rel n1, Rel n2 -> n1 == n2
@@ -1146,8 +1207,8 @@ 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,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
-      ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2
+    | Case (ci1,p1,iv1,c1,bl1), Case (ci2,p2,iv2,c2,bl2) ->
+      ci1 == ci2 && p1 == p2 && invert_eqeq iv1 iv2 && c1 == c2 && array_eqeq bl1 bl2
     | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
       Int.equal i1 i2
       && Array.equal Int.equal ln1 ln2
@@ -1236,12 +1297,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         let u', hu = sh_instance u in
         (Construct (sh_construct c, u'),
          combinesmall 11 (combine (constructor_syntactic_hash c) hu))
-      | Case (ci,p,c,bl) ->
+      | Case (ci,p,iv,c,bl) ->
         let p, hp = sh_rec p
+        and iv, hiv = sh_invert iv
         and c, hc = sh_rec c in
         let bl,hbl = hash_term_array bl in
-        let hbl = combine (combine hc hp) hbl in
-        (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl)
+        let hbl = combine4 hc hp hiv hbl in
+        (Case (sh_ci ci, p, 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
@@ -1271,6 +1333,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         (t, combinesmall 18 (combine h l))
       | Float f -> (t, combinesmall 19 (Float64.hash f))
 
+  and sh_invert = function
+    | NoInvert -> NoInvert, 0
+    | CaseInvert {univs;args;} ->
+      let univs, hu = sh_instance univs in
+      let args, ha = hash_term_array args in
+      CaseInvert {univs;args;}, combinesmall 1 (combine hu ha)
+
   and sh_rec t =
     let (y, h) = hash_term t in
     (* [h] must be positive. *)
@@ -1332,8 +1401,8 @@ let rec hash t =
       combinesmall 10 (combine (ind_hash ind) (Instance.hash u))
     | Construct (c,u) ->
       combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
-    | Case (_ , p, c, bl) ->
-      combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl))
+    | Case (_ , p, iv, c, bl) ->
+      combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl))
     | Fix (_ln ,(_, tl, bl)) ->
       combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
     | CoFix(_ln, (_, tl, bl)) ->
@@ -1345,6 +1414,11 @@ let rec hash t =
     | Int i -> combinesmall 18 (Uint63.hash i)
     | Float f -> combinesmall 19 (Float64.hash f)
 
+and hash_invert = function
+  | NoInvert -> 0
+  | CaseInvert {univs;args;} ->
+    combinesmall 1 (combine (Instance.hash univs) (hash_term_array args))
+
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
 
@@ -1476,9 +1550,9 @@ let rec debug_print c =
   | Construct (((sp,i),j),u) ->
       str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
   | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")"
-  | Case (_ci,p,c,bl) -> v 0
+  | Case (_ci,p,iv,c,bl) -> v 0
       (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++
-             debug_print c ++ str"of") ++ cut() ++
+             debug_print c ++ debug_invert iv ++ str"of") ++ cut() ++
        prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++
       cut() ++ str"end")
   | Fix f -> debug_print_fix debug_print f
@@ -1492,3 +1566,9 @@ let rec debug_print c =
          str"}")
   | Int i -> str"Int("++str (Uint63.to_string i) ++ str")"
   | Float i -> str"Float("++str (Float64.to_string i) ++ str")"
+
+and debug_invert = let open Pp in function
+  | NoInvert -> mt()
+  | CaseInvert {univs;args;} ->
+    spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++
+    str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} "
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 00051d7551..0c151bb43c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -49,6 +49,14 @@ type case_info =
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
+type ('constr, 'univs) case_invert =
+  | NoInvert
+  (** Normal reduction: match when the scrutinee is a constructor. *)
+
+  | CaseInvert of { univs : 'univs; args : 'constr array; }
+  (** Reduce when the indices match those of the unique constructor.
+      (SProp to non SProp only) *)
+
 (** {6 The type of constructions } *)
 
 type t
@@ -148,7 +156,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr
 
     [ac]{^ ith} element is ith constructor case presented as
     {e lambda construct_args (without params). case_term } *)
-val mkCase : case_info * constr * constr * constr array -> constr
+val mkCase : case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array -> constr
 
 (** If [recindxs = [|i1,...in|]]
       [funnames = [|f1,.....fn|]]
@@ -232,7 +240,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 
   | Ind       of (inductive * 'univs)                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
   | Construct of (constructor * 'univs)              (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
-  | Case      of case_info * 'constr * 'constr * 'constr array
+  | Case      of case_info * 'constr * ('constr,'univs) case_invert * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -339,7 +347,7 @@ Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
 return P in t1], or [if c then t1 else t2])
 @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
 where [info] is pretty-printing information *)
-val destCase : constr -> case_info * constr * constr * constr array
+val destCase : constr -> case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array
 
 (** Destructs a projection *)
 val destProj : constr -> Projection.t * constr
@@ -497,12 +505,16 @@ val fold_with_full_binders :
   (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
     'a -> 'b -> constr -> 'b
 
+val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
+
 (** [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
 
 val map : (constr -> constr) -> constr -> constr
 
+val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert
+
 (** [map_user_view f c] maps [f] on the immediate subterms of [c]; it
    differs from [map f c] in that the typing context and body of the
    return predicate and of the branches of a [match] are considered as
@@ -514,6 +526,9 @@ val map_user_view : (constr -> constr) -> constr -> constr
 
 val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
 
+val fold_map_invert : ('a -> 'b -> 'a * 'b) ->
+  'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert
+
 (** [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
    index) which is processed by [g] (which typically add 1 to [n]) at
@@ -529,6 +544,8 @@ val map_with_binders :
 
 val iter : (constr -> unit) -> constr -> unit
 
+val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> unit
+
 (** [iter_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
    index) which is processed by [g] (which typically add 1 to [n]) at
@@ -558,7 +575,7 @@ val compare_head : constr constr_compare_fn -> constr constr_compare_fn
 (** Convert a global reference applied to 2 instances. The int says
    how many arguments are given (as we can only use cumulativity for
    fully applied inductives/constructors) .*)
-type 'univs instance_compare_fn = GlobRef.t -> int ->
+type 'univs instance_compare_fn = (GlobRef.t * int) option ->
   'univs -> 'univs -> bool
 
 (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
@@ -605,6 +622,9 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
   constr constr_compare_fn ->
   constr constr_compare_fn
 
+val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool)
+  -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool
+
 (** {6 Hashconsing} *)
 
 val hash : constr -> int
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index a17aff9b09..fdcf44c943 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,23 +75,30 @@ let share_univs cache r u l =
   let (u', args) = share cache r l in
     mkApp (instantiate_my_gr r (Instance.append u' u), args)
 
-let update_case_info cache ci modlist =
-  try
-    let (_u,l) = share cache (IndRef ci.ci_ind) modlist in
-    { ci with ci_npar = ci.ci_npar + Array.length l }
-  with Not_found ->
-    ci
+let update_case cache ci iv modlist =
+  match share cache (IndRef ci.ci_ind) modlist with
+  | exception Not_found -> ci, iv
+  | u, l ->
+    let iv = match iv with
+      | NoInvert -> NoInvert
+      | CaseInvert {univs; args;} ->
+        let univs = Instance.append u univs in
+        let args = Array.append l args in
+        CaseInvert {univs; args;}
+    in
+    { ci with ci_npar = ci.ci_npar + Array.length l }, iv
 
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
 
 let expmod_constr cache modlist c =
   let share_univs = share_univs cache in
-  let update_case_info = update_case_info cache in
+  let update_case = update_case cache in
   let rec substrec c =
     match kind c with
-      | Case (ci,p,t,br) ->
-          Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))
+      | Case (ci,p,iv,t,br) ->
+        let ci,iv = update_case ci iv modlist in
+        Constr.map substrec (mkCase (ci,p,iv,t,br))
 
       | Ind (ind,u) ->
           (try
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 2f6a870c8a..68bd1cbac9 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -94,6 +94,10 @@ type typing_flags = {
 
   cumulative_sprop : bool;
   (** SProp <= Type *)
+
+  allow_uip: bool;
+  (** Allow definitional UIP (breaks termination) *)
+
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 0ab99cab35..3de2cb00a4 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -27,6 +27,7 @@ let safe_flags oracle = {
   enable_native_compiler = true;
   indices_matter = true;
   cumulative_sprop = false;
+  allow_uip = false;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 182ed55d0e..0ae6f242f6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -449,6 +449,7 @@ let same_flags {
      enable_VM;
      enable_native_compiler;
      cumulative_sprop;
+     allow_uip;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -458,7 +459,8 @@ let same_flags {
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
   enable_native_compiler == alt.enable_native_compiler &&
-  cumulative_sprop == alt.cumulative_sprop
+  cumulative_sprop == alt.cumulative_sprop &&
+  allow_uip == alt.allow_uip
 [@warning "+9"]
 
 let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index e9687991c0..179353d3f0 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -134,11 +134,18 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) =
     (* Empty type: all OK *)
     | 0 -> univ_info
 
-    (* SProp primitive records are OK, if we squash and become fakerecord also OK *)
-    | 1 when isrecord -> univ_info
-
-    (* Unit and identity types must squash if SProp *)
-    | 1 -> check_univ_leq env_ar_par Univ.Universe.type0m univ_info
+    | 1 ->
+      (* SProp primitive records are OK, if we squash and become fakerecord also OK *)
+      if isrecord then univ_info
+      (* 1 constructor with no arguments also OK in SProp (to make
+         things easier on ourselves when reducing we forbid letins) *)
+      else if (Environ.typing_flags env_ar_par).allow_uip
+           && fst (splayed_lc.(0)) = []
+           && List.for_all Context.Rel.Declaration.is_local_assum params
+      then univ_info
+      (* 1 constructor with arguments must squash if SProp
+         (we could allow arguments in SProp but the reduction rule is a pain) *)
+      else check_univ_leq env_ar_par Univ.Universe.type0m univ_info
 
     (* More than 1 constructor: must squash if Prop/SProp *)
     | _ -> check_univ_leq env_ar_par Univ.Universe.type0 univ_info
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8423813639..c51d82ce07 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -756,7 +756,7 @@ let rec subterm_specif renv stack t =
   let f,l = decompose_app (whd_all renv.env t) in
     match kind f with
     | Rel k -> subterm_var k renv
-    | Case (ci,p,c,lbr) ->
+    | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *)
        let stack' = push_stack_closures renv l stack in
        let cases_spec =
          branches_specif renv (lazy_subterm_specif renv [] c) ci
@@ -954,7 +954,7 @@ let check_one_fix renv recpos trees def =
                       check_rec_call renv stack (Term.applist(lift p c,l))
               end
 
-        | Case (ci,p,c_0,lrest) ->
+        | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *)
             begin try
               List.iter (check_rec_call renv []) (c_0::p::l);
               (* compute the recarg info for the arguments of each branch *)
@@ -976,7 +976,7 @@ let check_one_fix renv recpos trees def =
                   (* the call to whd_betaiotazeta will reduce the
                      apparent iota redex away *)
                   check_rec_call renv []
-                    (Term.applist (mkCase (ci,p,c_0,lrest), l))
+                    (Term.applist (mkCase (ci,p,iv,c_0,lrest), l))
               | _ -> Exninfo.iraise exn
             end
 
@@ -1254,7 +1254,7 @@ let check_one_cofix env nbfix def deftype =
             else
               raise (CoFixGuardError (env,UnguardedRecursiveCall c))
 
-        | Case (_,p,tm,vrest) ->
+        | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *)
            begin
              let tree = match restrict_spec env (Subterm (Strict, tree)) p with
              | Dead_code -> assert false
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 662ad550b8..71a3e95d25 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -139,6 +139,11 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
     infer_stack infos variances stk
 
+  | FCaseInvert (_,p,_,_,br,e) ->
+    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
+
   (* Removed by whnf *)
   | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 317141e324..2aeb1ea202 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -364,20 +364,21 @@ 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,p,ct,l) ->
+      | Case (ci,p,iv,ct,l) ->
           let ci_ind =
             let (kn,i) = ci.ci_ind in
             let kn' = f kn in
             if kn'==kn then ci.ci_ind else kn',i
           in
           let p' = func p in
+          let iv' = map_invert func iv in
           let ct' = func ct in
           let l' = Array.Smart.map func l in
-            if (ci.ci_ind==ci_ind && p'==p
+            if (ci.ci_ind==ci_ind && p'==p && iv'==iv
                 && l'==l && ct'==ct)then c
             else
               mkCase ({ci with ci_ind = ci_ind},
-                      p',ct', l')
+                      p',iv',ct', l')
       | Cast (ct,k,t) ->
           let ct' = func ct in
           let t'= func t in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f30ddce4d7..c8cee7db73 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2088,7 +2088,7 @@ let compile_deps env sigma prefix ~interactive init t =
   | Proj (p,c) ->
     let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
     aux env lvl init c
-  | Case (ci, _p, _c, _ac) ->
+  | Case (ci, _p, _iv, _c, _ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
       fold_constr_with_binders succ (aux env) lvl init t
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 02ee501f5f..3819cfd8ee 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -521,7 +521,7 @@ let rec lambda_of_constr cache env sigma c =
     let prefix = get_mind_prefix env (fst ind) in
     mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
-  | Case(ci,t,a,branches) ->
+  | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
     let (mind,i as ind) = ci.ci_ind in
     let mib = lookup_mind mind env in
     let oib = mib.mind_packets.(i) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4ff90dd70d..e4b0bb17d4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -209,12 +209,16 @@ type conv_pb =
 
 let is_cumul = function CUMUL -> true | CONV -> false
 
-type 'a universe_compare =
-  { (* Might raise NotConvertible *)
-    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
-    compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
-      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
+type 'a universe_compare = {
+  (* used in reduction *)
+  compare_graph : 'a -> UGraph.t;
+
+  (* Might raise NotConvertible *)
+  compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+  compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+  compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+    Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+}
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -302,7 +306,6 @@ let unfold_ref_with_args infos tab fl v =
 
 type conv_tab = {
   cnv_inf : clos_infos;
-  relevances : Sorts.relevance Range.t;
   lft_tab : clos_tab;
   rgt_tab : clos_tab;
 }
@@ -313,13 +316,13 @@ type conv_tab = {
     passed to each respective side of the conversion function below. *)
 
 let push_relevance infos r =
-  { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances }
+  { infos with cnv_inf = CClosure.push_relevance infos.cnv_inf r }
 
 let push_relevances infos nas =
-  { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas }
+  { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas }
 
 let rec skip_pattern infos relevances n c1 c2 =
-  if Int.equal n 0 then {infos with relevances}, c1, c2
+  if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2
   else match kind c1, kind c2 with
     | Lambda (x, _, c1), Lambda (_, _, c2) ->
       skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
@@ -327,11 +330,11 @@ let rec skip_pattern infos relevances n c1 c2 =
 
 let skip_pattern infos n c1 c2 =
   if Int.equal n 0 then infos, c1, c2
-  else skip_pattern infos infos.relevances n c1 c2
+  else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2
 
 let is_irrelevant infos lft c =
   let env = info_env infos.cnv_inf in
-  try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
+  try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -633,12 +636,20 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
+    | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
+      (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
+      let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
+      let ccnv = ccnv CONV l2r infos el1 el2 in
+      let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
+      Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv)
+        br1 br2 cuniv
+
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
-     | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
+     | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ | FCaseInvert _
         | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
@@ -711,10 +722,10 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
 
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
-  let infos = create_clos_infos ~evars reds env in
+  let graph = (snd univs).compare_graph (fst univs) in
+  let infos = create_clos_infos ~univs:graph ~evars reds env in
   let infos = {
     cnv_inf = infos;
-    relevances = Range.empty;
     lft_tab = create_tab ();
     rgt_tab = create_tab ();
   } in
@@ -759,10 +770,25 @@ let check_inductive_instances cv_pb variance u1 u2 univs =
   else raise NotConvertible
 
 let checked_universes =
-  { compare_sorts = checked_sort_cmp_universes;
+  { compare_graph = (fun x -> x);
+    compare_sorts = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
     compare_cumul_instances = check_inductive_instances; }
 
+let () =
+  let conv infos tab a b =
+    try
+      let univs = info_univs infos in
+      let infos = { cnv_inf = infos; lft_tab = tab; rgt_tab = tab; } in
+      let univs', _ = ccnv CONV false infos el_id el_id a b
+          (univs, checked_universes)
+      in
+      assert (univs==univs');
+      true
+      with NotConvertible -> false
+  in
+  CClosure.set_conv conv
+
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
   else
@@ -807,7 +833,8 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
   (univs, Univ.Constraint.union csts csts')
 
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
-  { compare_sorts = infer_cmp_universes;
+  { compare_graph = (fun (x,_) -> x);
+    compare_sorts = infer_cmp_universes;
     compare_instances = infer_convert_instances;
     compare_cumul_instances = infer_inductive_instances; }
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ff5934c66c..4ae3838691 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,12 +36,15 @@ type 'a extended_conversion_function =
 
 type conv_pb = CONV | CUMUL
 
-type 'a universe_compare =
-  { (* Might raise NotConvertible *)
-    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
-    compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
-      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
+type 'a universe_compare = {
+  compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *)
+
+  (* Might raise NotConvertible *)
+  compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+  compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+  compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+    Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+}
 
 type 'a universe_state = 'a * 'a universe_compare
 
diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml
index 3f3e722245..3dd965aca4 100644
--- a/kernel/relevanceops.ml
+++ b/kernel/relevanceops.ml
@@ -61,7 +61,7 @@ let rec relevance_of_fterm env extra lft f =
       | FProj (p, _) -> relevance_of_projection env p
       | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance
       | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
-      | FCaseT (ci, _, _, _, _) -> ci.ci_relevance
+      | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance
       | FLambda (len, tys, bdy, e) ->
         let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
         let lft = Esubst.el_liftn len lft in
@@ -97,7 +97,7 @@ and relevance_of_term_extra env extra lft subs c =
   | App (c, _) -> relevance_of_term_extra env extra lft subs c
   | Const (c,_) -> relevance_of_constant env c
   | Construct (c,_) -> relevance_of_constructor env c
-  | Case (ci, _, _, _) -> ci.ci_relevance
+  | Case (ci, _, _, _, _) -> ci.ci_relevance
   | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (p, _) -> relevance_of_projection env p
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 42fc6b2e45..ae5c4b6880 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -68,6 +68,7 @@ type ('constr, 'types) ptype_error =
   | UndeclaredUniverse of Level.t
   | DisallowedSProp
   | BadRelevance
+  | BadInvert
 
 type type_error = (constr, types) ptype_error
 
@@ -159,6 +160,9 @@ let error_disallowed_sprop env =
 let error_bad_relevance env =
   raise (TypeError (env, BadRelevance))
 
+let error_bad_invert env =
+  raise (TypeError (env, BadInvert))
+
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
 | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -202,3 +206,4 @@ let map_ptype_error f = function
 | UndeclaredUniverse l -> UndeclaredUniverse l
 | DisallowedSProp -> DisallowedSProp
 | BadRelevance -> BadRelevance
+| BadInvert -> BadInvert
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index a58d9aa50d..b1f7eb8a34 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error =
   | UndeclaredUniverse of Level.t
   | DisallowedSProp
   | BadRelevance
+  | BadInvert
 
 type type_error = (constr, types) ptype_error
 
@@ -143,5 +144,7 @@ val error_disallowed_sprop : env -> 'a
 
 val error_bad_relevance : env -> 'a
 
+val error_bad_invert : env -> 'a
+
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 19d76bfee6..58a099f7f6 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -407,7 +407,20 @@ let check_branch_types env (ind,u) c ct lft explft =
     | Invalid_argument _ ->
         error_number_branches env (make_judge c ct) (Array.length explft)
 
-let type_of_case env ci p pt c ct _lf lft =
+let should_invert_case env ci =
+  ci.ci_relevance == Sorts.Relevant &&
+  let mib,mip = lookup_mind_specif env ci.ci_ind in
+  mip.mind_relevance == Sorts.Irrelevant &&
+  (* NB: it's possible to have 2 ctors or arguments to 1 ctor by unsetting univ checks
+     but we don't do special reduction in such cases
+
+     XXX Someday consider more carefully what happens with letin params and arguments
+     (currently they're squashed, see indtyping)
+ *)
+  Array.length mip.mind_nf_lc = 1 &&
+  List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt
+
+let type_of_case env ci p pt iv c ct _lf lft =
   let (pind, _ as indspec) =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct) in
@@ -418,6 +431,14 @@ let type_of_case env ci p pt c ct _lf lft =
     else (warn_bad_relevance_ci (); {ci with ci_relevance=rp})
   in
   let () = check_case_info env pind rp 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)
+    then error_bad_invert env
+  in
   let (bty,rslty) =
     type_case_branches env indspec (make_judge p pt) c in
   let () = check_branch_types env pind c ct lft bty in
@@ -564,13 +585,22 @@ let rec execute env cstr =
     | Construct c ->
       cstr, type_of_constructor env c
 
-    | Case (ci,p,c,lf) ->
+    | Case (ci,p,iv,c,lf) ->
         let c', ct = execute env c in
+        let iv' = match iv with
+          | NoInvert -> NoInvert
+          | CaseInvert {univs;args} ->
+            let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in
+            let (ct', _) : constr * Sorts.t = execute_is_type env ct' in
+            let () = conv_leq false env ct ct' in
+            let _, args' = decompose_appvect ct' in
+            if args == args' then iv else CaseInvert {univs;args=args'}
+        in
         let p', pt = execute env p in
         let lf', lft = execute_array env lf in
-        let ci', t = type_of_case env ci p' pt c' ct lf' lft in
-        let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr
-          else mkCase(ci',p',c',lf')
+        let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in
+        let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr
+          else mkCase(ci',p',iv',c',lf')
         in
         cstr, t
 
@@ -710,10 +740,10 @@ let judge_of_inductive env indu =
 let judge_of_constructor env cu =
   make_judge (mkConstructU cu) (type_of_constructor env cu)
 
-let judge_of_case env ci pj cj lfj =
+let judge_of_case env ci pj iv cj lfj =
   let lf, lft = dest_judgev lfj in
-  let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in
-  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t
+  let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in
+  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t
 
 (* Building type of primitive operators and type *)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e61d5c399e..65531ed38a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
 (** {6 Type of Cases. } *)
 val judge_of_case : env -> case_info
-  -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-    -> unsafe_judgment
+  -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment
+  -> unsafe_judgment array
+  -> unsafe_judgment
 
 (** {6 Type of global references. } *)
 
@@ -128,3 +129,7 @@ val type_of_prim : env -> CPrimitives.t -> types
 
 val warn_bad_relevance_name : string
 (** Allow the checker to make this warning into an error. *)
+
+val should_invert_case : env -> 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 a4465c293b..63d88c659a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -252,6 +252,12 @@ let subst_univs_level_constr subst c =
          let u' = Univ.subst_univs_level_universe subst u in
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
+      | Case (ci,p,CaseInvert {univs;args},c,br) ->
+        if Univ.Instance.is_empty univs then Constr.map aux t
+        else
+          let univs' = f univs in
+          if univs' == univs then Constr.map aux t
+          else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)))
       | _ -> Constr.map aux t
     in
     let c' = aux c in
@@ -288,6 +294,10 @@ let subst_instance_constr subst c =
          let u' = Univ.subst_instance_universe subst u in
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
+      | Case (ci,p,CaseInvert {univs;args},c,br) ->
+        let univs' = f univs in
+        if univs' == univs then Constr.map aux t
+        else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))
       | _ -> Constr.map aux t
     in
     aux c