UIP in SProp

20 files changed, 148 insertions, 98 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 25353b7c12..a459229256 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1131,14 +1131,14 @@ 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,p,c,brs) ->
+  | Case (ci,p,iv,c,brs) ->
       (* We traverse a split *)
       let p =
         let sign,p = decompose_lam_assum sigma p in
         let sign2,p = decompose_prod_n_assum sigma ng p in
         let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in
         it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
-      mkCase (ci,p,c,Array.map2 (fun q c ->
+      mkCase (ci,p,iv,c,Array.map2 (fun q c ->
         let sign,b = decompose_lam_n_decls sigma q c in
         it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign)
         ci.ci_cstr_ndecls brs)
@@ -1161,7 +1161,7 @@ let rec is_dependent_generalization sigma ng body =
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
       is_dependent_generalization sigma ng c
-  | Case (ci,p,c,brs) ->
+  | Case (ci,p,iv,c,brs) ->
       (* We traverse a split *)
       Array.exists2 (fun q c ->
         let _,b = decompose_lam_n_decls sigma q c in
@@ -1448,7 +1448,7 @@ let compile ~program_mode sigma pb =
             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 pred = nf_betaiota !!(pb.env) sigma pred in
-            let case = make_case_or_project !!(pb.env) sigma indf ci pred current brvals in
+            let case = make_case_or_project !!(pb.env) sigma indt ci pred current brvals in
             let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
             sigma, { uj_val = applist (case, inst);
               uj_type = prod_applist sigma typ inst }
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index b39ec37cd1..b713d7812e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -75,7 +75,8 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
+            * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 (* les vars pourraient etre des constr,
@@ -134,7 +135,7 @@ let rec stack_concat stk1 stk2 =
   match stk1 with
       TOP -> stk2
     | APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
-    | CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2)
+    | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2)
     | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2)
 
 (* merge stacks when there is no shifts in between *)
@@ -339,9 +340,9 @@ let rec reify_stack t = function
   | TOP -> t
   | APP (args,st) ->
       reify_stack (mkApp(t,Array.map reify_value args)) st
-  | CASE (ty,br,ci,env,st) ->
+  | CASE (ty,br,iv,ci,env,st) ->
       reify_stack
-        (mkCase (ci, ty, t,br))
+        (mkCase (ci, ty, iv, t, br))
         st
   | PROJ (p, st) ->
        reify_stack (mkProj (p, t)) st
@@ -400,7 +401,7 @@ let rec norm_head info env t stack =
                         they could be computed when getting out of the stack *)
       let nargs = Array.map (cbv_stack_term info TOP env) args in
       norm_head info env head (stack_app nargs stack)
-  | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
+  | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack))
   | Cast (ct,_,_) -> norm_head info env ct stack
 
   | Proj (p, c) ->
@@ -514,14 +515,14 @@ and cbv_stack_value info env = function
         cbv_stack_term info stk envf redfix
 
     (* constructor in a Case -> IOTA *)
-    | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
+    | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk)))
             when red_set info.reds fMATCH ->
         let cargs =
           Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
-    | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
+    | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk))
             when red_set info.reds fMATCH ->
                     cbv_stack_term info stk env br.(n-1)
 
@@ -597,9 +598,9 @@ let rec apply_stack info t = function
   | TOP -> t
   | APP (args,st) ->
       apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
-  | CASE (ty,br,ci,env,st) ->
+  | CASE (ty,br,iv,ci,env,st) ->
       apply_stack info
-        (mkCase (ci, cbv_norm_term info env ty, t,
+        (mkCase (ci, cbv_norm_term info env ty, iv, t,
                     Array.map (cbv_norm_term info env) br))
         st
   | PROJ (p, st) ->
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index fdd4370613..d7804edf6d 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -41,7 +41,8 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
+            * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 val shift_value : int -> cbv_value -> cbv_value
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 25aa8915ba..656739657d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,7 +351,7 @@ let matches_core env sigma allow_bound_rels
           sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
-      | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
+      | PIf (a1,b1,b1'), Case (ci,_,_,a2,[|b2;b2'|]) ->
           let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in
           let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in
           let n = Context.Rel.length ctx_b2 in
@@ -367,7 +367,7 @@ let matches_core env sigma allow_bound_rels
           else
             raise PatternMatchingFailure
 
-      | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
+      | PCase (ci1,p1,a1,br1), Case (ci2,p2,_,a2,br2) ->
           let n2 = Array.length br2 in
           let () = match ci1.cip_ind with
           | None -> ()
@@ -498,9 +498,9 @@ let sub_match ?(closed=true) env sigma pat c =
        | [app';c] -> mk_ctx (mkApp (app',[|c|]))
        | _ -> assert false in
      try_aux [(env, app); (env, Array.last lc)] mk_ctx next
-  | Case (ci,hd,c1,lc) ->
+  | Case (ci,hd,iv,c1,lc) ->
       let next_mk_ctx = function
-      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc))
       | _ -> assert false
       in
       let sub = (env, c1) :: (env, hd) :: subargs env lc in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 13946208bc..02c04c2300 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -429,7 +429,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,p,c,cl) when
+    | Case (ci,p,iv,c,cl) when
         eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
         && not (Int.equal (Array.length cl) 0)
         && (* don't contract if p dependent *)
@@ -498,40 +498,46 @@ let it_destRLambda_or_LetIn_names l c =
               | _ -> DAst.make @@ GApp (c,[a]))
   in aux l [] c
 
-let detype_case computable detype detype_eqns testdep avoid data p c bl =
-  let (indsp,st,constagsl,k) = data in
+let detype_case computable detype detype_eqns testdep avoid ci p iv c bl =
   let synth_type = synthetize_type () in
   let tomatch = detype c in
+  let tomatch = match iv with
+    | NoInvert -> tomatch
+    | CaseInvert {univs;args} ->
+      let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+      DAst.make @@ GCast (tomatch, CastConv (detype t))
+  in
   let alias, aliastyp, pred=
     if (not !Flags.raw_print) && synth_type && computable && not (Int.equal (Array.length bl) 0)
     then
       Anonymous, None, None
     else
       let p = detype p in
-      let nl,typ = it_destRLambda_or_LetIn_names k p in
+      let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in
       let n,typ = match DAst.get typ with
         | GLambda (x,_,t,c) -> x, c
         | _ -> Anonymous, typ in
       let aliastyp =
         if List.for_all (Name.equal Anonymous) nl then None
-        else Some (CAst.make (indsp,nl)) in
+        else Some (CAst.make (ci.ci_ind,nl)) in
       n, aliastyp, Some typ
   in
-  let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
-  let tag =
+  let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in
+  let tag = let st = ci.ci_pp_info.style in
     try
       if !Flags.raw_print then
         RegularStyle
       else if st == LetPatternStyle then
         st
-      else if PrintingLet.active indsp then
+      else if PrintingLet.active ci.ci_ind then
         LetStyle
-      else if PrintingIf.active indsp then
+      else if PrintingIf.active ci.ci_ind then
         IfStyle
       else
         st
     with Not_found -> st
   in
+  let constagsl = ci.ci_pp_info.cstr_tags in
   match tag, aliastyp with
   | LetStyle, None ->
       let bl' = Array.map detype bl in
@@ -793,14 +799,12 @@ and detype_r d flags avoid env sigma t =
         GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
         GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u)
-    | Case (ci,p,c,bl) ->
+    | Case (ci,p,iv,c,bl) ->
         let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
         detype_case comp (detype d flags avoid env sigma)
           (detype_eqns d flags avoid env sigma ci comp)
           (is_nondep_branch sigma) avoid
-          (ci.ci_ind,ci.ci_pp_info.style,
-           ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
-          p c bl
+          ci p iv c bl
     | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef
     | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
     | Int i -> GInt i
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 366203faeb..0206d4e70d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -208,7 +208,7 @@ let occur_rigidly flags env evd (evk,_) t =
       if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true
       else Reducible
     | Rel _ | Var _ -> Reducible
-    | Case (_,_,c,_) ->
+    | Case (_,_,_,c,_) ->
       (match aux c with
       | Rigid b -> Rigid b
       | _ -> Reducible)
@@ -382,7 +382,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else None, x in
     match sk1, sk2 with
     | [], [] -> None, Success i
-    | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
+    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       (match f env i CONV t1 t2 with
       | Success i' ->
         (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
@@ -417,7 +417,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
   let rec ise_stack2 i sk1 sk2 =
     match sk1, sk2 with
     | [], [] -> Success i
-    | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
+    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       ise_and i [
       (fun i -> ise_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 908b8b00d6..98cfbf7fa7 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -78,7 +78,7 @@ and kind_of_head env t =
   | App (c,al) -> aux k (Array.to_list al @ l) c b
   | Proj (p,c) -> RigidHead RigidOther
 
-  | Case (_,_,c,_) -> aux k [] c true
+  | Case (_,_,_,c,_) -> aux k [] c true
   | Int _ | Float _ -> ConstructorHead
   | Fix ((i,j),_) ->
       let n = i.(j) in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6132365b27..0e7fac35f1 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -119,8 +119,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
       in
       let obj =
         match projs with
-        | None -> mkCase (ci, lift ndepar p,  mkRel 1,
-                          Termops.rel_vect ndepar k)
+        | None ->
+          let iv = make_case_invert env (find_rectype env sigma (EConstr.of_constr (lift 1 depind))) ci in
+          let iv = EConstr.Unsafe.to_case_invert iv in
+          mkCase (ci, lift ndepar p, iv, mkRel 1, Termops.rel_vect ndepar k)
         | Some ps ->
           let term =
             mkApp (mkRel 2,
@@ -407,7 +409,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
                   arsign'
               in
               let obj =
-                Inductiveops.make_case_or_project env !evdref indf ci (EConstr.of_constr pred)
+                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)
               in
               let obj = EConstr.to_constr !evdref obj in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e77c5082dd..23145b1629 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -66,6 +66,8 @@ let relevance_of_inductive_family env ((ind,_),_ : inductive_family) =
 
 type inductive_type = IndType of inductive_family * EConstr.constr list
 
+let ind_of_ind_type = function IndType (((ind,_),_),_) -> ind
+
 let make_ind_type (indf, realargs) = IndType (indf,realargs)
 let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
 
@@ -332,16 +334,26 @@ let get_constructors env (ind,params) =
 
 let get_projections = Environ.get_projections
 
-let make_case_or_project env sigma indf ci pred c branches =
+let make_case_invert env (IndType (((ind,u),params),indices)) ci =
+  if Typeops.should_invert_case env ci
+  then
+    let univs = EConstr.EInstance.make u in
+    let params = Array.map_of_list EConstr.of_constr params in
+    let args = Array.append params (Array.of_list indices) in
+    CaseInvert {univs;args}
+  else NoInvert
+
+let make_case_or_project env sigma indt ci pred c branches =
   let open EConstr in
-  let projs = get_projections env (fst (fst indf)) in
+  let IndType (((ind,_),_),_) = indt in
+  let projs = get_projections env ind in
   match projs with
-  | None -> (mkCase (ci, pred, c, branches))
+  | None ->
+    mkCase (ci, pred, make_case_invert env indt ci, c, branches)
   | Some ps ->
      assert(Array.length branches == 1);
      let na, ty, t = destLambda sigma pred in
      let () =
-       let (ind, _), _ = dest_ind_family indf in
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (Vars.noccurn sigma 1 t) &&
           not (has_dependent_elim mib) then
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 2bec86599e..1e2bba9f73 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -48,6 +48,7 @@ val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type ->
 val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
 val lift_inductive_type  : int -> inductive_type -> inductive_type
 val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type
+val ind_of_ind_type : inductive_type -> inductive
 
 val relevance_of_inductive_type : env -> inductive_type -> Sorts.relevance
 
@@ -204,9 +205,12 @@ val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_i
     Fail with an error if the elimination is dependent while the
     inductive type does not allow dependent elimination. *)
 val make_case_or_project :
-  env -> evar_map -> inductive_family -> case_info ->
+  env -> evar_map -> inductive_type -> case_info ->
   (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
 
+val make_case_invert : env -> inductive_type -> case_info
+  -> (EConstr.constr,EConstr.EInstance.t) case_invert
+
 (*i Compatibility
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index d672ddc906..89bd7e196f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -317,6 +317,11 @@ and nf_atom_type env sigma atom =
   | Avar id ->
       mkVar id, Typeops.type_of_variable env id
   | Acase(ans,accu,p,bs) ->
+      let () = if Typeops.should_invert_case env ans.asw_ci then
+          (* TODO implement case inversion readback (properly reducing
+             it is a problem for the kernel) *)
+          CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.")
+      in
       let a,ta = nf_accu_type env sigma accu in
       let ((mind,_),u as ind),allargs = find_rectype_a env ta in
       let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
@@ -338,8 +343,7 @@ and nf_atom_type env sigma atom =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs a in
-      let ci = ans.asw_ci in
-      mkCase(ci, p, a, branchs), tcase
+      mkCase(ans.asw_ci, p, NoInvert, 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 6d30e0338e..4aedeb43e3 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -193,8 +193,8 @@ let pattern_of_constr env sigma t =
          else PEvar (evk,List.map (pattern_of_constr env) ctxt)
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ ->
-         PMeta None)
-    | Case (ci,p,a,br) ->
+        PMeta None)
+    | Case (ci,p,_,a,br) ->
         let cip =
           { cip_style = ci.ci_pp_info.style;
             cip_ind = Some ci.ci_ind;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1b6c17fcf9..e4403d5bf4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -991,7 +991,7 @@ struct
     let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
     let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
     let sigma, cj = pretype empty_tycon env sigma c in
-    let (IndType (indf,realargs)) =
+    let (IndType (indf,realargs)) as indty =
       try find_rectype !!env sigma cj.uj_type
       with Not_found ->
         let cloc = loc_of_glob_constr c in
@@ -1028,11 +1028,11 @@ struct
     let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in
     let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
-    let obj ind rci p v f =
+    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 (fst ind) rci LetStyle in
-          mkCase (ci, p, cj.uj_val,[|f|])
+        let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in
+          mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|])
       else it_mkLambda_or_LetIn f fsign
     in
     (* Make dependencies from arity signature impossible *)
@@ -1060,7 +1060,7 @@ struct
             let v =
               let ind,_ = dest_ind_family indf in
                 let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in
-                obj ind rci p cj.uj_val fj.uj_val
+                obj indty rci p cj.uj_val fj.uj_val
             in
             sigma, { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) }
 
@@ -1079,7 +1079,7 @@ struct
             let v =
               let ind,_ = dest_ind_family indf in
                 let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in
-                obj ind rci p cj.uj_val fj.uj_val
+                obj indty rci p cj.uj_val fj.uj_val
             in sigma, { uj_val = v; uj_type = ccl })
 
   let pretype_cases self (sty, po, tml, eqns)  =
@@ -1092,7 +1092,7 @@ struct
     let open Context.Rel.Declaration in
     let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
     let sigma, cj = pretype empty_tycon env sigma c in
-    let (IndType (indf,realargs)) =
+    let (IndType (indf,realargs)) as indty =
       try find_rectype !!env sigma cj.uj_type
       with Not_found ->
         let cloc = loc_of_glob_constr c in
@@ -1148,7 +1148,7 @@ struct
         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 (ci, pred, cj.uj_val, [|b1;b2|])
+          mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|])
       in
       let cj = { uj_val = v; uj_type = p } in
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8ab040b3b1..18a0637efa 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -179,7 +179,7 @@ sig
 
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array
+  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -231,7 +231,7 @@ struct
 
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array
+  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -244,7 +244,7 @@ struct
     let pr_c x = hov 1 (pr_c x) in
     match member with
     | App app -> str "ZApp" ++ pr_app_node pr_c app
-    | Case (_,_,br) ->
+    | Case (_,_,_,br) ->
        str "ZCase(" ++
          prvect_with_sep (pr_bar) pr_c br
        ++ str ")"
@@ -285,7 +285,7 @@ struct
         ([],[]) -> Int.equal bal 0
       | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
-      | (Case(c1,_,_)::s1, Case(c2,_,_)::s2) ->
+      | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
       | (Proj (p)::s1, Proj(p2)::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
@@ -305,7 +305,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 (_,t1,a1) :: q1, Case (_,t2,a2) :: q2 ->
+      | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 ->
         aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
       | Proj (p1) :: q1, Proj (p2) :: q2 ->
         aux o q1 q2
@@ -321,7 +321,8 @@ struct
                                | App (i,a,j) ->
                                   let le = j - i + 1 in
                                   App (0,Array.map f (Array.sub a i le), le-1)
-                               | Case (info,ty,br) -> Case (info, f ty, Array.map f br)
+                               | Case (info,ty,iv,br) ->
+                                 Case (info, f ty, map_invert f iv, Array.map f br)
                                | Fix ((r,(na,ty,bo)),arg) ->
                                   Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg)
                                | Primitive (p,c,args,kargs) ->
@@ -403,7 +404,7 @@ struct
                 then a
                 else Array.sub a i (j - i + 1) in
        zip (mkApp (f, a'), s)
-    | f, (Case (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s)
+    | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
   | f, (Fix (fix,st)::s) -> zip
     (mkFix fix, st @ (append_app [|f|] s))
   | f, (Proj (p)::s) -> zip (mkProj (p,f),s)
@@ -536,12 +537,13 @@ let reduce_and_refold_cofix recfun env sigma cofix sk =
 let reduce_mind_case sigma mia =
   match EConstr.kind sigma mia.mconstr with
     | Construct ((ind_sp,i),u) ->
-(*	let ncargs = (fst mia.mci).(i-1) in*)
+(*      let ncargs = (fst mia.mci).(i-1) in*)
         let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
     | CoFix cofix ->
         let cofix_def = contract_cofix sigma cofix in
-        mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
+        (* XXX Is NoInvert OK here? *)
+        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
@@ -805,8 +807,8 @@ let rec whd_state_gen flags env sigma =
         | _ -> fold ())
       | _ -> fold ())
 
-    | Case (ci,p,d,lf) ->
-      whrec (d, Stack.Case (ci,p,lf) :: stack)
+    | Case (ci,p,iv,d,lf) ->
+      whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -819,7 +821,7 @@ let rec whd_state_gen flags env sigma =
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, lf)::s') when use_match ->
+        |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
           whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
         |args, (Stack.Proj (p)::s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
@@ -901,8 +903,8 @@ let local_whd_state_gen flags _env sigma =
     | Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
       (whrec (c, Stack.Proj (p) :: stack))
 
-    | Case (ci,p,d,lf) ->
-      whrec (d, Stack.Case (ci,p,lf) :: stack)
+    | Case (ci,p,iv,d,lf) ->
+      whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -920,7 +922,7 @@ let local_whd_state_gen flags _env sigma =
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, lf)::s') when use_match ->
+        |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
           whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
         |args, (Stack.Proj (p) :: s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
@@ -1035,7 +1037,7 @@ let clos_norm_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
     EConstr.of_constr (CClosure.norm_val
-      (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env)
       (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
@@ -1044,7 +1046,7 @@ let clos_whd_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
     EConstr.of_constr (CClosure.whd_val
-      (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env)
       (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
@@ -1148,7 +1150,8 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
 
 let sigma_univ_state =
   let open Reduction in
-  { compare_sorts = sigma_compare_sorts;
+  { compare_graph = Evd.universes;
+    compare_sorts = sigma_compare_sorts;
     compare_instances = sigma_compare_instances;
     compare_cumul_instances = sigma_check_inductive_instances; }
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index a0cbd8ccf7..58fff49faa 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -58,7 +58,7 @@ module Stack : sig
 
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array
+  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5ec5005b3e..bb518bc2f9 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -121,7 +121,7 @@ let retype ?(polyprop=true) sigma =
     | Evar ev -> existential_type sigma ev
     | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u))
     | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u))
-    | Case (_,p,c,lf) ->
+    | Case (_,p,_iv,c,lf) ->
         let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
@@ -297,7 +297,7 @@ let relevance_of_term env sigma c =
       | Const (c,_) -> Relevanceops.relevance_of_constant env c
       | Ind _ -> Sorts.Relevant
       | Construct (c,_) -> Relevanceops.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, _) -> Relevanceops.relevance_of_projection env p
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5b9bc91b84..baa32565f6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -277,8 +277,8 @@ let compute_consteval_direct env sigma ref =
       | Fix fix when not onlyproj ->
           (try check_fix_reversibility sigma labs l fix
           with Elimconst -> NotAnElimination)
-      | Case (_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
-      | Case (_,_,d,_) -> srec env n labs true d
+      | Case (_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
+      | Case (_,_,_,d,_) -> srec env n labs true d
       | Proj (p, d) when isRel sigma d -> EliminationProj n
       | _ -> NotAnElimination
   in
@@ -538,7 +538,8 @@ let reduce_mind_case_use_function func env sigma mia =
             fun _ -> None in
         let cofix_def =
           contract_cofix_use_function env sigma build_cofix_name cofix in
-        mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
+        (* Is NoInvert OK here? *)
+        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 
@@ -573,7 +574,7 @@ let match_eval_ref_value env sigma constr stack =
      env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
   | _ -> None
 
-let special_red_case env sigma whfun (ci, p, c, lf) =
+let special_red_case env sigma whfun (ci, p, iv, c, lf) =
   let rec redrec s =
     let (constr, cargs) = whfun s in
     match match_eval_ref env sigma constr cargs with
@@ -619,9 +620,9 @@ let reduce_proj env sigma whfun whfun' c =
           let proj_narg = Projection.npars proj + Projection.arg proj in
           List.nth cargs proj_narg
         | _ -> raise Redelimination)
-    | Case (n,p,c,brs) ->
+    | Case (n,p,iv,c,brs) ->
       let c' = redrec c in
-      let p = (n,p,c',brs) in
+      let p = (n,p,iv,c',brs) in
         (try special_red_case env sigma whfun' p
          with Redelimination -> mkCase p)
     | _ -> raise Redelimination
@@ -772,9 +773,9 @@ and whd_simpl_stack env sigma =
       | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack))
       | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
       | Cast (c,_,_) -> redrec (applist(c, stack))
-      | Case (ci,p,c,lf) ->
+      | Case (ci,p,iv,c,lf) ->
           (try
-            redrec (applist(special_red_case env sigma redrec (ci,p,c,lf), stack))
+            redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack))
           with
               Redelimination -> s')
       | Fix fix ->
@@ -867,7 +868,7 @@ let try_red_product env sigma c =
           let open Context.Rel.Declaration in
           mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b)
       | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
-      | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
+      | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf))
       | Proj (p, c) ->
         let c' =
           match EConstr.kind sigma c with
@@ -1264,10 +1265,10 @@ let one_step_reduce env sigma c =
       | App (f,cl) -> redrec (f, (Array.to_list cl)@stack)
       | LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack)
       | Cast (c,_,_) -> redrec (c,stack)
-      | Case (ci,p,c,lf) ->
+      | Case (ci,p,iv,c,lf) ->
           (try
              (special_red_case env sigma (whd_simpl_stack env sigma)
-               (ci,p,c,lf), stack)
+               (ci,p,iv,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
           (try match reduce_fix (whd_construct_stack env) sigma fix stack with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f0882d4594..b4a1153731 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c =
   let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
   sigma, (lc, ty, Sorts.relevance_of_sort ps)
 
-let judge_of_case env sigma ci pj cj lfj =
+let judge_of_case env sigma ci pj 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
@@ -186,7 +186,10 @@ let judge_of_case env sigma ci pj cj lfj =
   let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec pj cj.uj_val in
   let () = check_case_info env (fst indspec) rci ci in
   let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in
-  sigma, { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
+  let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
+    then Type_errors.error_bad_invert env
+  in
+  sigma, { uj_val  = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj);
            uj_type = rslty }
 
 let check_type_fixpoint ?loc env sigma lna lar vdefj =
@@ -361,11 +364,20 @@ let rec execute env sigma cstr =
         let sigma, ty = type_of_constructor env sigma ctor in
         sigma, make_judge cstr ty
 
-    | Case (ci,p,c,lf) ->
+    | Case (ci,p,iv,c,lf) ->
         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
-        judge_of_case env sigma ci pj cj lfj
+        let sigma = match iv with
+          | NoInvert -> sigma
+          | CaseInvert {univs;args} ->
+            let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+            let sigma, tj = execute env sigma t in
+            let sigma, tj = type_judgment env sigma tj in
+            let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in
+            sigma
+        in
+        judge_of_case env sigma ci pj iv cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
         let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 95b07e227e..ef58f41489 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -567,7 +567,7 @@ let is_rigid_head sigma flags t =
   | Construct _ | Int _ | Float _ -> true
   | Fix _ | CoFix _ -> true
   | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
-    | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _)
+    | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _)
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c =
@@ -657,7 +657,7 @@ let rec is_neutral env sigma ts t =
       not (TransparentState.is_transparent_variable ts id)
     | Rel n -> true
     | Evar _ | Meta _ -> true
-    | Case (_, p, c, cl) -> is_neutral env sigma ts c
+    | Case (_, p, _, c, _) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
     | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
@@ -847,7 +847,7 @@ 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,p1,c1,cl1), Case (ci2,p2,c2,cl2) ->
+        | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
             (try
              if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
              let opt' = {opt with at_top = true; with_types = false} in
@@ -1782,7 +1782,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
                  matchrec c1
                with ex when precatchable_exception ex ->
                  matchrec c2)
-          | Case(_,_,c,lf) -> (* does not search in the predicate *)
+          | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
                (try
                  matchrec c
                with ex when precatchable_exception ex ->
@@ -1867,7 +1867,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
                 let c2 = args.(n-1) in
                 bind (matchrec c1) (matchrec c2)
 
-            | Case(_,_,c,lf) -> (* does not search in the predicate *)
+            | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
                 bind (matchrec c) (bind_iter matchrec lf)
 
             | Proj (p,c) -> matchrec c
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 37c34d55cf..efe1efd74e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -261,6 +261,12 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
       assert (from = 0) ;
+      let ci = sw.sw_annot.Vmvalues.ci in
+      let () = if Typeops.should_invert_case env ci then
+          (* TODO implement case inversion readback (properly reducing
+             it is a problem for the kernel) *)
+          CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.")
+      in
       let ((mind,_ as ind), u), allargs = find_rectype_a env t in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
@@ -280,8 +286,7 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs c in
-      let ci = sw.sw_annot.Vmvalues.ci in
-      nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
+      nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk
   | Zproj p :: stk ->
      assert (from = 0) ;
      let p' = Projection.make p true in