diff options
| author | Hugo Herbelin | 2019-11-13 12:26:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-30 18:59:26 +0100 |
| commit | bc5e44cafa1a4040e4e4f2ad84ff6df36ab99446 (patch) | |
| tree | 9540ef1c282bb85cc3779b673dd9b7606999aba0 /interp/constrextern.ml | |
| parent | 012e5de12947e774fff59316487c77cf94c12961 (diff) | |
Printing tests for applied references combined with impl. args. and notations.
This shows a few bugs and even anomalies. See issue #11091.
See further commits for some fixes.
Diffstat (limited to 'interp/constrextern.ml')
0 files changed, 0 insertions, 0 deletions