From 593e99514abc1b43a011f4ae64f40443714b0a68 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 30 Jun 2020 18:03:14 +0200
Subject: [record] [ci] Overlay for elpi

We re-expose `declare_projections` and `declare_structure_entry` as it
is needed by coq-elpi.

Ideally we would provide a better way in recordops to interact with
this, in fact `declare_structure_entry` is just a wrapper around
recordops + libobject structure so there is hope it goes away entirely
in the future.

The need for Elpi to manually call `declare_projections` should
actually disappear in future refactorings.
---
 .../12611-ejgallego-record+refactor.sh             |  9 +++++++++
 vernac/record.ml                                   |  9 +++++++++
 vernac/record.mli                                  | 23 ++++++++++++++++++++--
 3 files changed, 39 insertions(+), 2 deletions(-)
 create mode 100644 dev/ci/user-overlays/12611-ejgallego-record+refactor.sh

diff --git a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh
new file mode 100644
index 0000000000..b7d21ed59c
--- /dev/null
+++ b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then
+
+    elpi_CI_REF=record+refactor
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+#    mtac2_CI_REF=record+refactor
+#    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/vernac/record.ml b/vernac/record.ml
index 6e024d08ca..4c9479f386 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -838,3 +838,12 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records
     class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data
   | Inductive_kw | CoInductive | Variant | Record | Structure ->
     regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data
+
+module Internal = struct
+  type nonrec projection_flags = projection_flags = {
+    pf_subclass: bool;
+    pf_canonical: bool;
+  }
+  let declare_projections = declare_projections
+  let declare_structure_entry = declare_structure_entry
+end
diff --git a/vernac/record.mli b/vernac/record.mli
index 86819a25ec..ffcae2975e 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -35,5 +35,24 @@ val definition_structure
 
 val declare_existing_class : GlobRef.t -> unit
 
-(** Used by elpi *)
-val declare_structure_entry : Recordops.struc_typ -> unit
+(* Implementation internals, consult Coq developers before using;
+   current user Elpi, see https://github.com/LPCIC/coq-elpi/pull/151 *)
+module Internal : sig
+  type projection_flags = {
+    pf_subclass: bool;
+    pf_canonical: bool;
+  }
+
+  val declare_projections
+    : Names.inductive
+    -> Entries.universes_entry
+    -> ?kind:Decls.definition_object_kind
+    -> Names.Id.t
+    -> projection_flags list
+    -> Impargs.manual_implicits list
+    -> Constr.rel_context
+    -> Recordops.proj_kind list * Names.Constant.t option list
+
+  val declare_structure_entry : Recordops.struc_typ -> unit
+
+end
-- 
cgit v1.2.3