diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-05-26 18:12:14 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-26 18:12:14 +0200 |
commit | 06aa7498415ca98a795219a2b1460e812b6bafc6 (patch) | |
tree | 7e6abfa81039608c59d1f53335afc68fd82b441a /lib/feedback.mli | |
parent | 9c8cdd5f6c1cb4bda2f8558c17df3ffe69c49264 (diff) | |
parent | 8bd3e4eba54ace61f49a53b8ce74517de71006ec (diff) |
Merge PR#655: Extra functions exported in EConstr
Diffstat (limited to 'lib/feedback.mli')
0 files changed, 0 insertions, 0 deletions