Merge pull request #568 from SkySkimmer/ci-relevance

Adapt to coq/coq#18280 (case relevance outside case info)

src/depelim.ml

@@ -165,7 +165,7 @@ let depcase ~poly ((mind, i as ind), u) =
         (make_assum (nameR (Id.of_string ("P" ^ string_of_int i))) br))
       oneind.mind_consnames oneind.mind_nf_lc
   in
-  let ci = make_case_info (Global.env ()) ind relevance RegularStyle in
+  let ci = make_case_info (Global.env ()) ind RegularStyle in
   let obj i =
     mkApp (mkIndU (ind,u),
           (Array.append (extended_rel_vect (nargs + nconstrs + i) params)
@@ -177,7 +177,7 @@ let depcase ~poly ((mind, i as ind), u) =
   in
   let paramsinst = extended_rel_vect (2 + nargs + nconstrs) params in
   let ty = (annot_of_context ctxpred, app) in
-  let case = mkCase (ci, EInstance.empty, paramsinst, ty, NoInvert, mkRel 1, bodies) in
+  let case = mkCase (ci, EInstance.empty, paramsinst, (ty, relevance), NoInvert, mkRel 1, bodies) in
   let xty = obj 1 in
   let xid = Namegen.named_hd (Global.env ()) !evd xty Anonymous in
   let body =

src/eqdec.ml

@@ -67,8 +67,8 @@ let inductive_info sigma ((mind, _ as ind),u) =
 	arities
     in
     let case c pred brs =
-      let ci = make_case_info (Global.env ()) (mind,i) Sorts.Relevant Constr.RegularStyle in
-      mkCase (EConstr.contract_case env sigma (ci, pred, Constr.NoInvert, c, brs))
+      let ci = make_case_info (Global.env ()) (mind,i) Constr.RegularStyle in
+      mkCase (EConstr.contract_case env sigma (ci, (pred, Sorts.Relevant), Constr.NoInvert, c, brs))
       (* TODO relevance / case inversion *)
     in
       { ind_name = indname;

src/noconf.ml

@@ -31,7 +31,7 @@ let mkcase env sigma c ty constrs =
   let ctx = CVars.subst_instance_context ui ctx in
   let _len = List.length ctx in
   let params = mindb.mind_nparams in
-  let ci = make_case_info env (fst ind) Sorts.Relevant RegularStyle in
+  let ci = make_case_info env (fst ind) RegularStyle in
   let brs = 
     Array.map2_i (fun i id (ctx, cty) ->
       let cty = Term.it_mkProd_or_LetIn cty ctx in
@@ -44,7 +44,7 @@ let mkcase env sigma c ty constrs =
       it_mkLambda_or_LetIn res args)
       oneind.mind_consnames oneind.mind_nf_lc
   in
-    make_case_or_project env sigma indty ci ty c brs
+    make_case_or_project env sigma indty ci (ty, Sorts.Relevant) c brs
 
 let mk_eq env env' evd args args' =
   let _, _, make = Sigma_types.telescope env evd args in

src/splitting.ml

@@ -650,10 +650,10 @@ let term_of_tree env0 isevar sort tree =
       let pind, args = find_inductive env !evd rel_ty in
 
       (* Build the case. *)
-      let case_info = Inductiveops.make_case_info env (fst pind) elim_relevance Constr.RegularStyle in
+      let case_info = Inductiveops.make_case_info env (fst pind) Constr.RegularStyle in
       let indty = Inductiveops.find_rectype env !evd (mkApp (mkIndU pind, Array.map_of_list EConstr.of_constr args)) in
       let case = Inductiveops.make_case_or_project env !evd indty case_info
-          case_ty rel_t branches in
+          (case_ty, elim_relevance) rel_t branches in
       let term = EConstr.mkApp (case, Array.of_list to_apply) in
       let term = EConstr.it_mkLambda_or_LetIn term ctx in
       let typ = it_mkProd_or_subst env evm ty ctx in

src/subterm.ml

@@ -374,9 +374,9 @@ let derive_below env sigma ~poly (ind,univ as indu) =
         (nargs, bodyB, bodyb)) oneind.mind_nf_lc
     in
     let caseB =
-      mkCase (EConstr.contract_case env !evd (make_case_info env ind Sorts.Relevant RegularStyle, aritylam, NoInvert, mkRel 1, Array.map pi2 branches))
+      mkCase (EConstr.contract_case env !evd (make_case_info env ind RegularStyle, (aritylam, Sorts.Relevant), NoInvert, mkRel 1, Array.map pi2 branches))
     and caseb =
-      mkCase (EConstr.contract_case env !evd (make_case_info env ind Sorts.Relevant RegularStyle, aritylamb, NoInvert, mkRel 1, Array.map pi3 branches))
+      mkCase (EConstr.contract_case env !evd (make_case_info env ind RegularStyle, (aritylamb, Sorts.Relevant), NoInvert, mkRel 1, Array.map pi3 branches))
     in 
       lift 2 (it_mkLambda_or_LetIn caseB argbinders), lift 3 (it_mkLambda_or_LetIn caseb argbinders)
   in