diff options
| author | Maxime Dénès | 2018-02-05 10:47:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-05 10:47:44 +0100 |
| commit | 55b2a4e0c24d691b71256c91ed54e245efce340b (patch) | |
| tree | 25c65622b9e9e83271d321f399981438b83ff053 /intf | |
| parent | f5cf5e062bdc6264dc3c398ad76559ec188cde47 (diff) | |
| parent | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (diff) | |
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8bd2da2f11..8e0fe54c55 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -167,6 +167,7 @@ type option_ref_value = type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option type sort_expr = Sorts.family @@ -204,12 +205,12 @@ type inductive_expr = type one_inductive_expr = ident_decl * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = (Name.t Loc.located * universe_decl_expr option) * binding_kind * constr_expr +type typeclass_constraint = name_decl * binding_kind * constr_expr and typeclass_context = typeclass_constraint list type proof_expr = - ident_decl option * (local_binder_expr list * constr_expr) + ident_decl * (local_binder_expr list * constr_expr) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -339,7 +340,7 @@ type nonrec vernac_expr = | VernacNotationAddFormat of string * string * string (* Gallina *) - | VernacDefinition of (discharge * definition_object_kind) * ident_decl * definition_expr + | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr | VernacStartTheoremProof of theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr @@ -449,7 +450,6 @@ type nonrec vernac_expr = | VernacComments of comment list (* Proof management *) - | VernacGoal of constr_expr | VernacAbort of lident option | VernacAbortAll | VernacRestart |