diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-27 18:29:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-27 18:29:39 +0200 |
| commit | c33988dafcad14f9f0c10a287d2cfb2790e253c4 (patch) | |
| tree | eba36b138067491f49fd12656df98d73ac8e7742 /engine | |
| parent | 04e0f9fde8789a28b66f24000ac8c831ff0815af (diff) | |
| parent | 8d9b66bed22364f513771e9b1fa3df14a3dab866 (diff) | |
Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions