Merge PR coq#17714: Stop returning Sorts.family from Inductiveops.get_arity

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

pretyping/cases.ml

@@ -941,7 +941,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl =
     match typ with
     | IsInd (_, IndType (_, _), []) -> []
     | IsInd (_, IndType (indf, realargs), names) ->
-       let arsign,_ = get_arity env indf in
+       let arsign = get_arity env indf in
        let arsign = List.map EConstr.of_rel_decl arsign in
        subst_of_rel_context_instance_list arsign realargs
     | NotInd _ -> [] in
@@ -1451,7 +1451,7 @@ let compile ~program_mode sigma pb =
         let mind,_ = dest_ind_family indf in
         let () = Tacred.check_privacy !!(pb.env) (fst mind) in
         let cstrs = get_constructors !!(pb.env) indf in
-        let arsign, _ = get_arity !!(pb.env) indf in
+        let arsign = get_arity !!(pb.env) indf in
         let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
         let no_cstr = Int.equal (Array.length cstrs) 0 in
         if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
@@ -1981,7 +1981,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
           let indf' = if dolift then lift_inductive_family n indf else indf in
           let ((ind,u),_) = dest_ind_family indf' in
           let nrealargs_ctxt = inductive_nrealdecls env0 ind in
-          let arsign, inds = get_arity env0 indf' in
+          let arsign = get_arity env0 indf' in
           let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
           let realnal =
             match t with
@@ -1993,7 +1993,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
                   List.rev realnal
               | None ->
                   List.make nrealargs_ctxt Anonymous in
-          let r = Sorts.relevance_of_sort_family inds in
+          let r = Inductive.relevance_of_inductive env0 ind in
           let t = EConstr.of_constr (build_dependent_inductive env0 indf') in
           LocalAssum (make_annot na r, t) :: List.map2 RelDecl.set_name realnal arsign in
   let rec buildrec n = function
@@ -2287,8 +2287,7 @@ let constr_of_pat env sigma arsign pat avoid =
               Anonymous ->
                 sigma, pat', sign, app, apptype, realargs, n, avoid
             | Name id ->
-                let _, inds = get_arity env indf in
-                let r = Sorts.relevance_of_sort_family inds in
+                let r = Inductiveops.relevance_of_inductive_family env indf in
                 let sign = LocalAssum (make_annot alias r, lift m ty) :: sign in
                 let avoid = Id.Set.add id avoid in
                 let sigma, sign, i, avoid =

pretyping/indrec.ml

@@ -187,8 +187,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib, mip) kind =
     let nbprod = Array.length mip.mind_consnames + 1 in
 
     let indf' = lift_inductive_family nbprod indf in
-    let arsign,sort = get_arity !!env indf' in
-    let r = Sorts.relevance_of_sort_family sort in
+    let arsign = get_arity !!env indf' in
+    let r = Inductiveops.relevance_of_inductive_family !!env indf' in
     let depind = build_dependent_inductive !!env indf' in
     let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in
 
@@ -448,8 +448,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
           let args = Context.Rel.instance_list mkRel (nrec+nbconstruct) lnamesparrec in
           let indf = make_ind_family((indi,u),args) in
 
-          let arsign,s = get_arity !!env indf in
-          let r = Sorts.relevance_of_sort_family s in
+          let arsign = get_arity !!env indf in
+          let r = Inductiveops.relevance_of_inductive_family !!env indf in
           let depind = build_dependent_inductive !!env indf in
           let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in
 
@@ -485,8 +485,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
             (* Predicate in the context of the case *)
 
             let depind' = build_dependent_inductive !!env indf' in
-            let arsign',s = get_arity !!env indf' in
-            let r = Sorts.relevance_of_sort_family s in
+            let arsign' = get_arity !!env indf' in
+            let r = Inductiveops.relevance_of_inductive_family !!env indf' in
             let deparsign' = LocalAssum (make_annot Anonymous r,depind')::arsign' in
 
             let pargs =

pretyping/inductiveops.ml

@@ -453,7 +453,7 @@ let get_arity env ((ind,u),params) =
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
   let subst = subst_of_rel_context_instance_list parsign params in
   let arsign = Vars.subst_instance_context u arsign in
-  (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
+  substl_rel_context subst arsign
 
 (* Functions to build standard types related to inductive *)
 let build_dependent_constructor cs =
@@ -463,17 +463,17 @@ let build_dependent_constructor cs =
       @(Context.Rel.instance_list mkRel 0 cs.cs_args))
 
 let build_dependent_inductive env ((ind, params) as indf) =
-  let arsign,_ = get_arity env indf in
+  let arsign = get_arity env indf in
   let nrealargs = List.length arsign in
   applist
     (mkIndU ind,
      (List.map (lift nrealargs) params)@(Context.Rel.instance_list mkRel 0 arsign))
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-let make_arity_signature env sigma dep indf =
-  let (arsign,s) = get_arity env indf in
-  let r = Sorts.relevance_of_sort_family s in
+let make_arity_signature env sigma dep ((ind,_), _ as indf) =
+  let arsign = get_arity env indf in
+  let r = Inductive.relevance_of_inductive env ind in
   let anon = make_annot Anonymous r in
   let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
   if dep then
@@ -621,8 +621,8 @@ let find_coinductive env sigma c =
 
 (* Type of Case predicates *)
 let arity_of_case_predicate env (ind,params) dep k =
-  let arsign,s = get_arity env (ind,params) in
-  let r = Sorts.relevance_of_sort_family s in
+  let arsign = get_arity env (ind,params) in
+  let r = Inductive.relevance_of_inductive env (fst ind) in
   let mind = build_dependent_inductive env (ind,params) in
   let concl = if dep then mkArrow mind r (mkSort k) else mkSort k in
   Term.it_mkProd_or_LetIn concl arsign

pretyping/inductiveops.mli

@@ -181,7 +181,7 @@ val get_constructors : env -> inductive_family -> constructor_summary array
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
     part of the inductive family, they appears in the arity *)
-val get_arity        : env -> inductive_family -> Constr.rel_context * Sorts.family
+val get_arity        : env -> inductive_family -> Constr.rel_context
 
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr

pretyping/pretyping.ml

@@ -1094,8 +1094,8 @@ struct
     in
     (* Make dependencies from arity signature impossible *)
     let arsgn, indr =
-      let arsgn,s = get_arity !!env indf in
-      List.map (set_name Anonymous) arsgn, Sorts.relevance_of_sort_family s
+      let arsgn = get_arity !!env indf in
+      List.map (set_name Anonymous) arsgn, Inductiveops.relevance_of_inductive_family !!env indf
     in
       let indt = build_dependent_inductive !!env indf in
       let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *)
@@ -1160,9 +1160,9 @@ struct
                       (str "If is only for inductive types with two constructors.");
 
       let arsgn, indr =
-        let arsgn,s = get_arity !!env indf in
+        let arsgn = get_arity !!env indf in
         (* Make dependencies from arity signature impossible *)
-        List.map (set_name Anonymous) arsgn, Sorts.relevance_of_sort_family s
+        List.map (set_name Anonymous) arsgn, Inductiveops.relevance_of_inductive_family !!env indf
       in
       let nar = List.length arsgn in
       let indt = build_dependent_inductive !!env indf in

proofs/clenv.ml

@@ -805,8 +805,8 @@ let build_case_analysis env sigma (ind, u) params pred indices indarg dep knd =
   let relevance = Sorts.relevance_of_sort knd in
 
   let pnas, deparsign =
-    let arsign, sort = get_arity env indf in
-    let r = Sorts.relevance_of_sort_family sort in
+    let arsign = get_arity env indf in
+    let r = Inductiveops.relevance_of_inductive_family env indf in
     let depind = build_dependent_inductive env indf in
     let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in
     let set_names env l =

tactics/inv.ml

@@ -85,7 +85,7 @@ let make_inv_predicate env evd indf realargs id status concl =
     match status with
       | NoDep ->
           (* We push the arity and leave concl unchanged *)
-          let hyps_arity,_ = get_arity env indf in
+          let hyps_arity = get_arity env indf in
           let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in
             (hyps_arity,concl)
       | Dep dflt_concl ->