diff options
| author | Pierre-Marie Pédrot | 2019-06-08 21:46:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-08 21:46:56 +0200 |
| commit | 27b6f605efb2e94656c3405ddc271a775fbdab7e (patch) | |
| tree | f01870646eaa3803ef96531fc2f1d6c04f5c5dfa /doc/plugin_tutorial/tuto0 | |
| parent | 65f75de6929530252a3235af54a0da56980fa02d (diff) | |
Fix #10339: Anomaly in Ltac2.
We use a user-facing wrapper instead of a low-level function raising internal
exceptions.
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions