Merge pull request #133 from SkySkimmer/cominductive-lbound

Adapt to rocq-prover/rocq#19985 (template poly has pseudo sort poly)

Author: ppedrot

src/parametricity.ml

@@ -1175,7 +1175,7 @@ let rec translate_mind_body name order evdr env kn b inst =
   | None -> None, mind_entry_params_R
   | Some temp ->
     let umap, univs, params = fix_template_params order evdr env temp b mind_entry_params_R in
-    Some (umap, univs), params
+    Some (umap, univs, temp.template_pseudo_sort_poly), params
   in
   debug_string [`Inductive] "translatation of inductive ...";
   let mind_entry_inds_R =
@@ -1188,15 +1188,15 @@ let rec translate_mind_body name order evdr env kn b inst =
     | Monomorphic ->
       begin match template_univs with
       | None -> Monomorphic_ind_entry
-      | Some (_, ctx) -> Template_ind_entry ctx
+      | Some (_, ctx, pseudo_sort_poly) -> Template_ind_entry { univs = ctx; pseudo_sort_poly }
       end
     | Polymorphic _ ->
       let uctx, _ = (Evd.univ_entry ~poly:true !evdr) in
       match uctx with Polymorphic_entry uctx -> Polymorphic_ind_entry uctx | _ -> assert false
   in
   let mind_entry_inds_R = match template_univs with
   | None -> mind_entry_inds_R
-  | Some (umap, _) ->
+  | Some (umap, _, _) ->
     let entry = match mind_entry_inds_R with
     | [entry] -> entry
     | _ -> assert false