From 6b258247becc59433d05f9a1f2ea5f05c30258bc Mon Sep 17 00:00:00 2001
From: Enzo Crance <enzo.crance@inria.fr>
Date: Mon, 21 Nov 2022 15:27:29 +0100
Subject: [PATCH] :bug: Fix declaration of upoly record projections

The call to Record.Internal.declare_projections was using Monomorphic_entry in any case, which prevented projections from being declared when the record was universe polymorphic.
---
 src/coq_elpi_builtins.ml | 11 ++++++-----
 tests/test_API_env.v     | 12 ++++++++++++
 2 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 644b5f8ff..6aca5bcb4 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -1863,16 +1863,17 @@ Supported attributes:
      if not (is_mutual_inductive_entry_ground me sigma) then
        err Pp.(str"coq.env.add-indt: the inductive type declaration must be ground. Did you forge to call coq.typecheck-indt-decl?");
      let primitive_expected = match record_info with Some(p, _) -> p | _ -> false in
-     let ubinders = 
+     let (uentry, uentry', ubinders) = 
        let open Entries in
        match me.mind_entry_universes with
-       | Monomorphic_ind_entry -> (UState.Monomorphic_entry uctx, univ_binders)
+       | Monomorphic_ind_entry -> (Monomorphic_entry, UState.Monomorphic_entry uctx, univ_binders)
        | Template_ind_entry _ -> nYI "template polymorphic inductives"
-       | Polymorphic_ind_entry uctx -> (UState.Polymorphic_entry uctx, univ_binders)
+       | Polymorphic_ind_entry uctx ->
+          (Polymorphic_entry uctx, UState.Polymorphic_entry uctx, univ_binders)
        in
      let () = DeclareUctx.declare_universe_context ~poly:false uctx in
      let mind =
-       DeclareInd.declare_mutual_inductive_with_eliminations ~primitive_expected me ubinders ind_impls in
+       DeclareInd.declare_mutual_inductive_with_eliminations ~primitive_expected me (uentry', ubinders) ind_impls in
      let ind = mind, 0 in
      begin match record_info with
      | None -> () (* regular inductive *)
@@ -1891,7 +1892,7 @@ Supported attributes:
          let fields_as_relctx = Term.prod_assum k_ty in
          let projections =
            Record.Internal.declare_projections ind ~kind:Decls.Definition
-             (Entries.Monomorphic_entry, UnivNames.empty_binders)
+             (uentry, ubinders)
              (Names.Id.of_string "record")
              flags is_implicit fields_as_relctx
          in
diff --git a/tests/test_API_env.v b/tests/test_API_env.v
index 6387d906a..ba04da37f 100644
--- a/tests/test_API_env.v
+++ b/tests/test_API_env.v
@@ -357,3 +357,15 @@ Elpi Query lp:{{
 
 }}.
 
+Set Universe Polymorphism.
+
+Elpi Query lp:{{
+  coq.env.begin-module "Test" none,
+  Decl = record "Rec" {{ Type }} "BuildRec" (field [] "f" {{ Type }} (_\ end-record)),
+  @univpoly! =>
+    coq.env.add-indt Decl _,
+  coq.env.end-module _.
+}}.
+
+Set Printing Universes. Print Module Test.
+Check Test.f.