diff options
| author | Hugo Herbelin | 2017-10-22 23:50:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-04 14:12:45 +0100 |
| commit | 8c6092e8c43a74a8a175a532580284124c06e34f (patch) | |
| tree | ece4db520837006b2e3bffcc165b7c76a45b1bd1 /API/API.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 'API/API.mli')
0 files changed, 0 insertions, 0 deletions