diff options
| author | Maxime Dénès | 2017-09-11 14:01:56 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-11 14:01:56 +0200 |
| commit | cc94172036789cfef28007f59510b7f17df5d45d (patch) | |
| tree | bc8f18ed22140496273fa53f2ad0f65bbd45de46 /API/API.mli | |
| parent | 4882288ba34ad0c47f950e733ae353a1b881df77 (diff) | |
| parent | 5241a3f69a0ff8c9d33a02d1cf3ebc7bcead8819 (diff) | |
Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificially restricted to a non-empty context).
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions