pretyping doesn't generate extra template poly constraints

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