From 48d4d730c2d33fcf31f087e25b247d9453b673b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 18 Jun 2024 15:15:08 +0200
Subject: [PATCH] pretyping doesn't generate extra template poly constraints

---
 pretyping/pretyping.ml | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a241f56ff7e78..b5c607e684158 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -923,6 +923,42 @@ struct
     let sigma, fj = pretype empty_tycon env sigma f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
+    let sigma, fj =
+      let template =
+        match EConstr.kind sigma fj.uj_val with
+        | Ind (ind,u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind !!env ->
+          Some (ind,None)
+        | Construct ((ind,ctor),u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind !!env ->
+          Some (ind,Some ctor)
+        | _ -> None
+      in
+      match template with
+      | None -> sigma, fj
+      | Some (ind,ctor) ->
+        let specif = Inductive.lookup_mind_specif !!env ind in
+        let sigma = ref sigma in
+        let param_univs = args |> List.map (fun arg ~expected ->
+            let sigma', u =
+              Evd.new_univ_level_variable ?loc:arg.CAst.loc UState.univ_flexible_alg !sigma
+            in
+            sigma := sigma';
+            TemplateUniv (Univ.Universe.make u))
+        in
+        let t, csts = match ctor with
+          | None ->
+            Inductive.type_of_inductive_knowing_parameters
+              (specif,UVars.Instance.empty)
+              param_univs
+          | Some ctor ->
+            Inductive.type_of_constructor_knowing_parameters
+              ((ind,ctor),UVars.Instance.empty)
+              specif
+              param_univs
+        in
+        let sigma = !sigma in
+        let sigma = Evd.add_constraints sigma csts in
+        sigma, { uj_val = fj.uj_val; uj_type = EConstr.of_constr t }
+    in
     let nargs_before_bidi =
       if Option.is_empty tycon then length
       (* We apply bidirectionality hints only if an expected type is specified *)
@@ -961,6 +997,7 @@ struct
     let refresh_template env sigma resj =
       (* Special case for inductive type applications that must be
          refreshed right away. *)
+      (* XXX still needed to make template work with Prop *)
       match EConstr.kind sigma resj.uj_val with
       | App (f,args) ->
         if Termops.is_template_polymorphic_ind !!env sigma f then