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 | |
| 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.
| -rw-r--r-- | dev/ci/user-overlays/12611-ejgallego-record+refactor.sh | 9 | ||||
| -rw-r--r-- | vernac/record.ml | 9 | ||||
| -rw-r--r-- | vernac/record.mli | 23 |
3 files changed, 39 insertions, 2 deletions
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 |