Merge PR #10390: UIP in SProp

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

10 files changed, 40 insertions, 32 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 52c6c5d0f9..23f8fe04a3 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -112,7 +112,7 @@ module Bool = struct
       else if head === negb && Array.length args = 1 then
         Negb (aux args.(0))
       else Var (Env.add env c)
-    | Case (info, r, arg, pats) ->
+    | Case (info, r, _iv, arg, pats) ->
       let is_bool =
         let i = info.ci_ind in
         Names.eq_ind i (Lazy.force ind)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0f96b9bbe8..a7c926f50c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -291,7 +291,7 @@ let rec extract_type env sg db j c args =
                       let reason = if lvl == TypeScheme then Ktype else Kprop in
                       Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop
+    | _ when info_of_family (sort_of env sg (applistc c args)) == Logic -> Tdummy Kprop
     | Rel n ->
         (match EConstr.lookup_rel n env with
            | LocalDef (_,t,_) ->
@@ -672,8 +672,9 @@ let rec extract_term env sg mle mlt c args =
         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
         let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
         in extract_app env sg mle mlt extract_rel args
-    | Case ({ci_ind=ip},_,c0,br) ->
-        extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
+    | Case ({ci_ind=ip},_,iv,c0,br) ->
+      (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
+      extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
         extract_app env sg mle mlt (extract_fix env sg mle i recd) args
     | CoFix (i,recd) ->
@@ -852,8 +853,8 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
   end else
     (* [c] has an inductive type, and is not a type scheme type. *)
     let t = type_of env sg c in
-    (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env sg t) == InProp then
+    (* The only non-informative case: [c] is of sort [Prop]/[SProp] *)
+    if info_of_family (sort_of env sg t) == Logic then
       begin
         add_recursors env kn; (* May have passed unseen if logical ... *)
         (* Logical singleton case: *)
@@ -1016,7 +1017,7 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map EConstr.mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env sg ti.(i) != InProp then
+    if info_of_family (sort_of env sg ti.(i)) != Logic then
       try
         let e,t = extract_std_constant env sg vkn.(i)
                    (EConstr.Vars.substl sub ci.(i)) ti.(i) in
@@ -1073,7 +1074,7 @@ let fake_match_projection env p =
       else
         let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
         let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
-        let body = mkCase (ci, p, mkRel 1, [|branch|]) in
+        let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in
         it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
     | LocalDef (_,c,t) :: rem ->
       let c = liftn 1 j c in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 9c3debe48f..c62bc73e41 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,10 @@ let unif env evd t1 t2=
           | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
           | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
               Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
-          | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
-              Queue.add (pa,pb) bige;
-              Queue.add (ca,cb) bige;
-              let l=Array.length va in
+          | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
+            Queue.add (pa,pb) bige;
+            Queue.add (ca,cb) bige;
+            let l=Array.length va in
                 if not (Int.equal l (Array.length vb)) then
                   raise (UFAIL (nt1,nt2))
                 else
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9b578d4697..f2658a395f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -585,10 +585,10 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
     let sigma = project g in
     (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
     match EConstr.kind sigma dyn_infos.info with
-    | Case (ci, ct, t, cb) ->
+    | Case (ci, ct, iv, t, cb) ->
       let do_finalize_t dyn_info' g =
         let t = dyn_info'.info in
-        let dyn_infos = {dyn_info' with info = mkCase (ci, ct, t, cb)} in
+        let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in
         let g_nb_prod = nb_prod (project g) (pf_concl g) in
         let g, type_of_term = tac_type_of g t in
         let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index dcca694200..f773157c52 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -987,7 +987,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
                   ( UnivGen.constr_of_monomorphic_global
                   @@ Coqlib.lib_ref "core.False.type" )) ->
         Proofview.V82.of_tactic tauto g
-      | Case (_, _, v, _) ->
+      | Case (_, _, _, v, _) ->
         tclTHENLIST
           [Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite]
           g
@@ -1026,7 +1026,7 @@ let rec reflexivity_with_destruct_cases g =
       match
         EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2)
       with
-      | Case (_, _, v, _) ->
+      | Case (_, _, _, v, _) ->
         tclTHENLIST
           [ Proofview.V82.of_tactic (simplest_case v)
           ; Proofview.V82.of_tactic intros
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 884792cc15..701ea56c2a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -312,7 +312,7 @@ let check_not_nested env sigma forbidden e =
     | Const _ -> ()
     | Ind _ -> ()
     | Construct _ -> ()
-    | Case (_, t, e, a) ->
+    | Case (_, t, _, e, a) ->
       check_not_nested t;
       check_not_nested e;
       Array.iter check_not_nested a
@@ -374,7 +374,13 @@ type journey_info =
   ; lambdA : (Name.t * types * constr, constr) journey_info_tac
   ; casE :
          ((constr infos -> tactic) -> constr infos -> tactic)
-      -> (case_info * constr * constr * constr array, constr) journey_info_tac
+      -> ( case_info
+           * constr
+           * (constr, EInstance.t) case_invert
+           * constr
+           * constr array
+         , constr )
+         journey_info_tac
   ; otherS : (unit, constr) journey_info_tac
   ; apP : (constr * constr list, constr) journey_info_tac
   ; app_reC : (constr * constr list, constr) journey_info_tac
@@ -474,9 +480,9 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
         ++ Printer.pr_leconstr_env env sigma expr_info.info
         ++ str " can not contain a recursive call to "
         ++ Id.print expr_info.f_id ) )
-  | Case (ci, t, a, l) ->
+  | Case (ci, t, iv, a, l) ->
     let continuation_tac_a =
-      jinfo.casE (travel jinfo) (ci, t, a, l) expr_info continuation_tac
+      jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
     in
     travel jinfo continuation_tac_a
       {expr_info with info = a; is_main_branch = false; is_final = false}
@@ -767,7 +773,8 @@ let mkDestructEq not_on_hyp expr g =
   in
   (g, tac, to_revert)
 
-let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
+let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
+    g =
   let sigma = project g in
   let env = pf_env g in
   let f_is_present =
@@ -779,7 +786,7 @@ let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
   let a' = infos.info in
   let new_info =
     { infos with
-      info = mkCase (ci, t, a', l)
+      info = mkCase (ci, t, iv, a', l)
     ; is_main_branch = expr_info.is_main_branch
     ; is_final = expr_info.is_final }
   in
@@ -916,10 +923,10 @@ let prove_terminate = travel terminate_info
 
 (* Equation proof *)
 
-let equation_case next_step (ci, a, t, l) expr_info continuation_tac infos =
+let equation_case next_step case expr_info continuation_tac infos =
   observe_tac
     (fun _ _ -> str "equation case")
-    (terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos)
+    (terminate_case next_step case expr_info continuation_tac infos)
 
 let rec prove_le g =
   let sigma = project g in
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 40c64a1c26..66c72a30a2 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -776,7 +776,7 @@ let rec find_a_destructable_match sigma t =
   let cl = [cl, (None, None), None], None in
   let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
   match EConstr.kind sigma t with
-    | Case (_,_,x,_) when closed0 sigma x ->
+    | Case (_,_,_,x,_) when closed0 sigma x ->
         if isVar sigma x then
           (* TODO check there is no rel n. *)
           raise (Found (Tacinterp.eval_tactic dest))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 40dea90c00..fb149071c9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -923,8 +923,8 @@ let reset_env env =
   let env' = Global.env_of_context (Environ.named_context_val env) in
     Environ.push_rel_context (Environ.rel_context env) env'
 
-let fold_match env sigma c =
-  let (ci, p, c, brs) = destCase sigma c in
+let fold_match ?(force=false) env sigma c =
+  let (ci, p, iv, c, brs) = destCase sigma c in
   let cty = Retyping.get_type_of env sigma c in
   let dep, pred, exists, sk =
     let env', ctx, body =
@@ -1184,7 +1184,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
           | Fail | Identity -> b'
         in state, res
 
-      | Case (ci, p, c, brs) ->
+      | Case (ci, p, iv, c, brs) ->
         let cty = Retyping.get_type_of env (goalevars evars) c in
         let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
         let cstr' = Some eqty in
@@ -1194,7 +1194,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
         let state, res =
           match c' with
           | Success r ->
-            let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
+            let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
             let res = make_leibniz_proof env case ty r in
               state, Success (coerce env unfresh (prop,cstr) res)
           | Fail | Identity ->
@@ -1216,7 +1216,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
               in
                 match found with
                 | Some r ->
-                  let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+                  let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in
                     state, Success (make_leibniz_proof env ctxc ty r)
                 | None -> state, c'
             else
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 878f7a834e..95faede7d0 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -77,7 +77,7 @@ let protect_red map env sigma c0 =
   let evars ev = Evarutil.safe_evar_value sigma ev in
   let c = EConstr.Unsafe.to_constr c0 in
   let tab = create_tab () in
-  let infos = create_clos_infos ~evars all env in
+  let infos = create_clos_infos ~univs:(Evd.universes sigma) ~evars all env in
   let map = lookup_map map sigma c0 in
   let rec eval n c = match Constr.kind c with
   | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u)
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 5d6e7c51d0..162013c556 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -308,7 +308,7 @@ let iter_constr_LR f c = match kind c with
   | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
   | LetIn (_, v, t, b) -> f v; f t; f b
   | App (cf, a) -> f cf; Array.iter f a
-  | Case (_, p, v, b) -> f v; f p; Array.iter f b
+  | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f b
   | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
   | Proj(_,a) -> f a