From 84a85f33ea41a6e05041e278acfa6fe348167d70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 17 Jan 2025 16:34:33 +0100
Subject: [PATCH] Adapt to coq/coq#19985 (template poly has pseudo sort poly)

---
 src/parametricity.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/parametricity.ml b/src/parametricity.ml
index 49d14a1..0a340a6 100644
--- 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,7 +1188,7 @@ 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
@@ -1196,7 +1196,7 @@ let rec translate_mind_body name order evdr env kn b inst =
   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