diff options
Diffstat (limited to 'toplevel/record.mli')
| -rw-r--r-- | toplevel/record.mli | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/toplevel/record.mli b/toplevel/record.mli index c2c6b72ee..7799162df 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -14,6 +14,7 @@ open Term open Sign open Vernacexpr open Topconstr +open Impargs (*i*) (* [declare_projections ref name coers params fields] declare projections of @@ -21,7 +22,18 @@ open Topconstr as coercions accordingly to [coers]; it returns the absolute names of projections *) val declare_projections : - inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list + inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> + bool list -> manual_explicitation list list -> rel_context -> + bool list * constant option list + +val declare_structure : identifier -> identifier -> + manual_explicitation list -> rel_context -> (* params *) + Term.constr -> (* arity *) + Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *) + ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> + bool -> (* coercion? *) + bool list -> (* field coercions *) + mutual_inductive val definition_structure : lident with_coercion * local_binder list * |