diff options
| author | Maxime Dénès | 2015-09-17 09:48:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-09-17 09:48:19 +0200 |
| commit | 13ea0a5011875e362aa388989b72b3f7ed0c505b (patch) | |
| tree | faa045035065875845cea1c80cbb3a3b4f624fbf /intf | |
| parent | f2f805ed8275f70767284f4d3c8a13db6f8c8923 (diff) | |
| parent | fbb3ccdb099170e5a39c9f39512b1ab2503951ea (diff) | |
Merge branch 'v8.5' into trunk
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 |