diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -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 f018d59e6..cb093d85d 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 |