[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.

1 files changed, 9 insertions, 0 deletions

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