diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 18:03:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-13 19:12:29 +0100 |
| commit | 593e99514abc1b43a011f4ae64f40443714b0a68 (patch) | |
| tree | a7c9b1f2fdd4a45d8e11c980be79a23618a8e73a /vernac | |
| parent | df19ab7cc9931580171ed910f6b2d15ff8247492 (diff) | |
[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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 9 | ||||
| -rw-r--r-- | vernac/record.mli | 23 |
2 files changed, 30 insertions, 2 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 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 |