diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 11:25:29 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 11:25:29 +0200 |
| commit | 66a68a4329ce199f25184ba8b2d98b4679e7ddae (patch) | |
| tree | ce90c93341c58e82813da8b1a567ce6a3f3ed424 /intf | |
| parent | 0a255f51809e8d29a7239bfbd9fe57a8b2b41705 (diff) | |
| parent | 2ddc9d12bd4616f10245c40bc0c87ae548911809 (diff) | |
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of let-ins
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 49bafadc8..a4a6eb909 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -19,7 +19,7 @@ open Decl_kinds type notation = string type explicitation = - | ExplByPos of int * Id.t option + | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) | ExplByName of Id.t type binder_kind = 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 |