Merge pull request #118 from SkySkimmer/ci-relevance

Adapt to rocq-prover/rocq#18280 (case relevance outside case info)

Author: ppedrot

src/parametricity.ml

@@ -398,9 +398,9 @@ and translate order evd env (t : constr) : constr =
     | Construct cstru -> translate_constructor order env evd cstru
 
     | Case (ci, u, pms, p, iv, c, bl) ->
-        let (ci, p, iv, c, bl) = EConstr.expand_case env !evd (ci, u, pms, p, iv, c, bl) in
+        let (ci, (p,r), iv, c, bl) = EConstr.expand_case env !evd (ci, u, pms, p, iv, c, bl) in
         let nargs, nparams = Inductiveops.inductive_nrealargs env ci.ci_ind, Inductiveops.inductive_nparams env ci.ci_ind in
-        let theta = mkCase (EConstr.contract_case env !evd (ci, lift (nargs + 1) p, Constr.map_invert (lift (nargs + 1)) iv, mkRel 1, Array.map (lift (nargs + 1)) bl)) in
+        let theta = mkCase (EConstr.contract_case env !evd (ci, (lift (nargs + 1) p, r), Constr.map_invert (lift (nargs + 1)) iv, mkRel 1, Array.map (lift (nargs + 1)) bl)) in
         debug_case_info [`Case] ci;
         debug [`Case] "theta (in translated env) = " Environ.empty_env !evd theta;
         debug_string [`Case] (Printf.sprintf "nargs = %d, params = %d" nargs nparams);
@@ -420,7 +420,7 @@ and translate order evd env (t : constr) : constr =
         let p_R = compose_lambda_decls lams_R t_R in
         let c_R = translate order evd env c in
         let bl_R = Array.map (translate order evd env) bl in
-        let tuple = (EConstr.contract_case env !evd (ci_R, p_R, Constr.NoInvert, c_R, bl_R)) in
+        let tuple = (EConstr.contract_case env !evd (ci_R, (p_R,r), Constr.NoInvert, c_R, bl_R)) in
         mkCase tuple
 
     | CoFix _ ->
@@ -544,7 +544,6 @@ and translate_case_info order env ci =
   {
     ci_ind = ci_ind;
     ci_npar = (order + 1) * ci.ci_npar;
-    ci_relevance = ci.ci_relevance;
     ci_cstr_ndecls = Array.map (fun x -> (order + 1) * x) ci.ci_cstr_ndecls;
     ci_cstr_nargs = Array.map (fun x -> (order + 1) * x) ci.ci_cstr_nargs;
     ci_pp_info = translate_case_printing order env ci.ci_pp_info;
@@ -764,7 +763,7 @@ and translate_fix order evd env t =
     and process_case env depth (fun_args : constr list) case =
 
         debug [`Fix] "case = " env !evd case;
-        let (ci, p, iv, c, bl) = EConstr.expand_case env !evd (destCase !evd case) in
+        let (ci, (p,r), iv, c, bl) = EConstr.expand_case env !evd (destCase !evd case) in
         debug [`Fix] "predicate = " env !evd p;
         let c_R = translate order evd env c in
         let ci_R = translate_case_info order env ci in
@@ -842,7 +841,7 @@ and translate_fix order evd env t =
             ) bl
           end
         in
-        mkCase (EConstr.contract_case env !evd (ci_R, p_R, iv, c_R, bl_R))
+        mkCase (EConstr.contract_case env !evd (ci_R, (p_R,r), iv, c_R, bl_R))
     in
     let (_, ft_R, bk, bk_R) = ftbk_R.(n) in
     let nfun_letins = nfun + narg - nrealargs.(n) in