diff options
| author | Matthieu Sozeau | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /intf | |
| parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) | |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index bb0331fcc4..37218fbf91 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -160,6 +160,9 @@ type option_ref_value = | StringRefValue of string | QualidRefValue of reference +(** Identifier and optional list of bound universes. *) +type plident = lident * lident list option + type sort_expr = glob_sort type definition_expr = @@ -168,10 +171,10 @@ type definition_expr = * constr_expr option type fixpoint_expr = - Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option type cofixpoint_expr = - Id.t located * local_binder list * constr_expr * constr_expr option + plident * local_binder list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -190,14 +193,14 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - lident with_coercion * local_binder list * constr_expr option * inductive_kind * + plident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - lident * local_binder list * constr_expr option * constructor_expr list + plident * local_binder list * constr_expr option * constructor_expr list type proof_expr = - lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) type grammar_tactic_prod_item_expr = | TacTerm of string @@ -305,7 +308,7 @@ type vernac_expr = (* Gallina *) | VernacDefinition of - (locality option * definition_object_kind) * lident * definition_expr + (locality option * definition_object_kind) * plident * definition_expr | VernacStartTheoremProof of theorem_kind * proof_expr list * bool | VernacEndProof of proof_end | VernacExactProof of constr_expr |