Merge pull request #133 from SkySkimmer/cominductive-lbound

Adapt to coq/coq#19985 (template poly has pseudo sort poly)
coq-community · Jan 23, 2025 · aac0331 · aac0331
2 parents 9c5fd9f + 84a85f3
commit aac0331
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/parametricity.ml b/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