diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-02 11:21:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-09 11:52:17 +0200 |
| commit | 1a43fda0dc9bb8d100808426980446353f8f1ae3 (patch) | |
| tree | 5907412903414e3c21d718a70dc0d377a3589b1a /intf | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
Removing internal support for accepting "{struct x}" and co in "Theorem with".
There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 25d3c705f..d62c639c2 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -209,7 +209,7 @@ type one_inductive_expr = plident * local_binder_expr list * constr_expr option * constructor_expr list type proof_expr = - plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder_expr list * constr_expr) type syntax_modifier = | SetItemLevel of string list * Extend.production_level |