diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-22 23:50:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-04 14:12:45 +0100 |
| commit | 8c6092e8c43a74a8a175a532580284124c06e34f (patch) | |
| tree | ece4db520837006b2e3bffcc165b7c76a45b1bd1 /plugins/ltac/tacexpr.mli | |
| parent | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (diff) | |
Adding support for syntax "let _ := e in e'" in Ltac.
Adding a file fixing #5996 and which uses this feature.
Diffstat (limited to 'plugins/ltac/tacexpr.mli')
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 163973688..9bd3efc6b 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -254,7 +254,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Id.t located * 'a gen_tactic_arg) list * + (Name.t located * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * |