diff options
| author | Hugo Herbelin | 2017-03-22 19:31:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-22 19:34:01 +0100 |
| commit | 947d93a8b7ff0fc7ba23633fcd44820427e29326 (patch) | |
| tree | 8257bdccc135ec71108ebfa1fc212951c9271abf /dev | |
| parent | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff) | |
Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.
This adds at least support for camlp5 6.14 (in addition to 6.17).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions