diff options
| -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 |