Adapt to rocq-prover/rocq#20102 (template poly api change)

Author: SkySkimmer

template-coq/src/run_template_monad.ml

@@ -282,7 +282,7 @@ let unquote_mutual_inductive_entry env evm trm (* of type mutual_inductive_entry
        let priv = unquote_map_option unquote_bool priv in
        let ctx, univs = match univs with
        | UState.Monomorphic_entry ctx ->
-          if template then Univ.ContextSet.empty, Entries.Template_ind_entry ctx
+          if template then Univ.ContextSet.empty, Entries.Template_ind_entry { univs = ctx; pseudo_sort_poly = TemplateUnivOnly }
           else ctx, Entries.Monomorphic_ind_entry
        | UState.Polymorphic_entry uctx -> Univ.ContextSet.empty, Entries.Polymorphic_ind_entry uctx
        in

template-coq/src/tm_util.ml

@@ -283,10 +283,10 @@ module RetypeMindEntry =
     let ctx, mind =
       match mind.mind_entry_universes with
       | Entries.Monomorphic_ind_entry ->
-        Evd.universe_context_set evm, { mind with mind_entry_universes = Entries.Monomorphic_ind_entry }
-      | Entries.Template_ind_entry ctx ->
-        Evd.universe_context_set evm, { mind with mind_entry_universes = Entries.Template_ind_entry ctx }
-      | Entries.Polymorphic_ind_entry uctx ->
+        Evd.universe_context_set evm, mind
+      | Entries.Template_ind_entry _ ->
+        Evd.universe_context_set evm, mind
+      | Entries.Polymorphic_ind_entry _ ->
         let uctx' = Evd.to_universe_context evm in
         Univ.ContextSet.empty, { mind with mind_entry_universes = Entries.Polymorphic_ind_entry uctx' }
     in ctx, mind