diff options
| author | Pierre-Marie Pédrot | 2020-04-09 23:29:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-07 00:22:11 +0200 |
| commit | c39b622a8d8b32f335ee7dfe56ad27f9db7caaee (patch) | |
| tree | 6b8bd1218e3c31d1c85dd1d89a8243f61d6157de /interp | |
| parent | f694d42400593d7ef3ad6c2812395f941cc4f5ca (diff) | |
Export API to recover values out of Ltac application.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions