Merge PR #10390: UIP in SProp

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

6 files changed, 34 insertions, 7 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 2bb4bac9a4..848cd501c6 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -179,7 +179,7 @@ let rec traverse current ctx accu t =
 | Construct (((mind, _), _) as cst, _) ->
   traverse_inductive accu mind (ConstructRef cst)
 | Meta _ | Evar _ -> assert false
-| Case (_,oty,c,[||]) ->
+| Case (_,oty,_,c,[||]) ->
     (* non dependent match on an inductive with no constructors *)
     begin match Constr.(kind oty, kind c) with
     | Lambda(_,_,oty), Const (kn, _)
@@ -306,6 +306,13 @@ let traverse current t =
     considering terms out of any valid environment, so use with caution. *)
 let type_of_constant cb = cb.Declarations.const_type
 
+let uses_uip mib =
+  Array.exists (fun mip ->
+      mip.mind_relevance == Sorts.Irrelevant
+      && Array.length mip.mind_nf_lc = 1
+      && List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt)
+    mib.mind_packets
+
 let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
   (* Only keep the transitive dependencies *)
   let (_, graph, ax2ty) = traverse (label_of gr) t in
@@ -363,5 +370,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
+      let accu =
+        if not (uses_uip mind) then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (UIP m, l)) Constr.mkProp accu
+      in
       accu
   in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index bb640a83f6..ef6f8652e9 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -350,13 +350,13 @@ let build_beq_scheme mode kn =
             done;
 
           ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
-                        (mkCase (ci,do_predicate rel_list nb_cstr_args,
+                        (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert,
                                   mkVar (Id.of_string "Y") ,ar2))
                          (constrsi.(i).cs_args))
         done;
         mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
           mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar)))
+            mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))
     in (* build_beq_scheme *)
     let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index f9b2d8b1d1..b9ed4f838d 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -66,9 +66,9 @@ let protect_pattern_in_binder bl c ctypopt =
         | LetIn (x,b,t,c) ->
           let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
           evd, mkLetIn (x,t,b,c)
-        | Case (ci,p,a,bl) ->
+        | Case (ci,p,iv,a,bl) ->
           let evd,bl = Array.fold_left_map (aux env) evd bl in
-          evd, mkCase (ci,p,a,bl)
+          evd, mkCase (ci,p,iv,a,bl)
         | Cast (c,_,_)    -> f env evd c  (* we remove the cast we had set *)
         (* This last case may happen when reaching the proof of an
            impossible case, as when pattern-matching on a vector of length 1 *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 0c4f76f682..f9ecf10d1b 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -736,6 +736,9 @@ let explain_disallowed_sprop () =
 let explain_bad_relevance env =
   strbrk "Bad relevance (maybe a bugged tactic)."
 
+let explain_bad_invert env =
+  strbrk "Bad case inversion (maybe a bugged tactic)."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -779,6 +782,7 @@ let explain_type_error env sigma err =
      explain_undeclared_universe env sigma l
   | DisallowedSProp -> explain_disallowed_sprop ()
   | BadRelevance -> explain_bad_relevance env
+  | BadInvert -> explain_bad_invert env
 
 let pr_position (cl,pos) =
   let clpos = match cl with
diff --git a/vernac/record.ml b/vernac/record.ml
index 3468f5fc36..820bcba0b6 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -343,8 +343,9 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
                      let p = mkLambda (x, lift 1 rp, ccl') in
                      let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
                      let ci = Inductiveops.make_case_info env indsp rci LetStyle in
-                     (* Record projections have no is *)
-                     mkCase (ci, p, mkRel 1, [|branch|]), None
+                     (* Record projections are always NoInvert because
+                        they're at constant relevance *)
+                     mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
                in
                let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
                let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 65af66435b..b0e483ee74 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1553,6 +1553,15 @@ let () =
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
       optwrite = (fun b -> Global.set_check_universes b) }
 
+let () =
+  declare_bool_option
+    { optdepr  = false;
+      optkey   = ["Definitional"; "UIP"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.allow_uip);
+      optwrite = (fun b -> Global.set_typing_flags
+                     {(Global.typing_flags ()) with Declarations.allow_uip = b})
+    }
+
 let vernac_set_strategy ~local l =
   let local = Option.default false local in
   let glob_ref r =