diff options
| author | Maxime Dénès | 2017-12-18 18:57:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 18:57:56 +0100 |
| commit | 7e2f9861f3d38829baf246883e4925d48c9e2998 (patch) | |
| tree | 17407cece435ac715b7918e1d5abf5e480ae74f6 /API/API.mli | |
| parent | 6af0969228e57c611e5a0876efe613055de342cd (diff) | |
| parent | a60a49f545499f29f067148668b8ec1bc7b55895 (diff) | |
Merge PR #6406: Make [abstract] nodes show up in the Ltac profile
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions