diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 22:33:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | e414c07e193db7d4256c09167f6efd545831fa2b (patch) | |
| tree | 116ddbcb55e13e723cc1c1af0c9627359f6998b2 /vernac/record.mli | |
| parent | 60770e86f4ec925fce52ad3565a92beb98d253c1 (diff) | |
Register universe binders for record projections.
Diffstat (limited to 'vernac/record.mli')
| -rw-r--r-- | vernac/record.mli | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/vernac/record.mli b/vernac/record.mli index 33c2fba89..9fdd5e1c4 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -7,36 +7,12 @@ (************************************************************************) open Names -open Constr open Vernacexpr open Constrexpr -open Impargs open Globnames val primitive_flag : bool ref -(** [declare_projections ref name coers params fields] declare projections of - record [ref] (if allowed) using the given [name] as argument, and put them - as coercions accordingly to [coers]; it returns the absolute names of projections *) - -val declare_projections : - inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> - coercion_flag list -> manual_explicitation list list -> Context.Rel.t -> - (Name.t * bool) list * Constant.t option list - -val declare_structure : - Decl_kinds.recursivity_kind -> - Entries.inductive_universes -> - Id.t -> Id.t -> - manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) - bool (** template arity ? *) -> - Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *) - ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t -> - bool -> (** coercion? *) - bool list -> (** field coercions *) - Evd.evar_map -> - inductive - val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * |