diff options
Diffstat (limited to 'toplevel/record.mli')
| -rw-r--r-- | toplevel/record.mli | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/toplevel/record.mli b/toplevel/record.mli index 9642b351..48181437 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: record.mli 11024 2008-05-30 12:41:39Z msozeau $ i*) +(*i $Id: record.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -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 * |