diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-11 14:01:56 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-11 14:01:56 +0200 |
| commit | cc94172036789cfef28007f59510b7f17df5d45d (patch) | |
| tree | bc8f18ed22140496273fa53f2ad0f65bbd45de46 /library/library.ml | |
| 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 'library/library.ml')
0 files changed, 0 insertions, 0 deletions