diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 02:43:42 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-13 19:12:29 +0100 |
| commit | b341b58104ff14f10a5e170d4bfbc7a02f12755f (patch) | |
| tree | 7e26fff0c0a96f4ba9e17facfa91a8336dfd9fda /vernac/record.mli | |
| parent | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (diff) | |
[record] Cleanup of data structure and functions [1/2]
In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.
The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.
Diffstat (limited to 'vernac/record.mli')
| -rw-r--r-- | vernac/record.mli | 30 |
1 files changed, 11 insertions, 19 deletions
diff --git a/vernac/record.mli b/vernac/record.mli index 38a622977a..c3b84540f0 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -14,20 +14,16 @@ open Constrexpr val primitive_flag : bool ref -type projection_flags = { - pf_subclass: bool; - pf_canonical: bool; -} - -val declare_projections : - inductive -> - Entries.universes_entry -> - ?kind:Decls.definition_object_kind -> - Id.t -> - projection_flags list -> - Impargs.manual_implicits list -> - Constr.rel_context -> - Recordops.proj_kind list * Constant.t option list +module Ast : sig + type t = + { name : Names.lident + ; is_coercion : coercion_flag + ; binders: local_binder_expr list + ; cfs : (local_decl_expr * record_field_attr) list + ; idbuild : Id.t + ; sort : constr_expr option + } +end val definition_structure : universe_decl_expr option @@ -36,11 +32,7 @@ val definition_structure -> cumulative:bool -> poly:bool -> Declarations.recursivity_kind - -> (coercion_flag * - Names.lident * - local_binder_expr list * - (local_decl_expr * record_field_attr) list * - Id.t * constr_expr option) list + -> Ast.t list -> GlobRef.t list val declare_existing_class : GlobRef.t -> unit |