diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /toplevel/record.mli | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 * |