diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 11:23:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 13:09:16 +0200 |
| commit | 7ee82cd2dfd8cb226c35c3094423e56c75010377 (patch) | |
| tree | 7a681820b8a475da703e025cc2e4a0182887604d /library/global.mli | |
| parent | f841c27c1cfd38aada72f3c8f90e2ed1ec22db6a (diff) | |
Backporting c064fb933 from 8.5 (another regression with Ltac trace report).
Doing it explicitly because it is in another file.
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions