diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-22 08:26:17 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-01 16:20:15 +0000 |
| commit | e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee (patch) | |
| tree | 4ed4ae97644642de2cda5eca4fd329889754e9b4 /intf | |
| parent | c658141acff6d1b7f610960dd39998385c7e8806 (diff) | |
[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8bd2da2f1..d954ae903 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,7 +205,7 @@ 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 @@ -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 |