diff options
| author | Pierre-Marie Pédrot | 2014-08-31 01:55:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-31 12:47:16 +0200 |
| commit | 29bb2f7d9fecf06e3246142e649db4db0320da41 (patch) | |
| tree | 569fae894aafaf91f64203bdb3ba5e8df176b5fd /kernel/type_errors.ml | |
| parent | 437b91a3ffd7327975a129b95b24d3f66ad7f3e4 (diff) | |
Moving code of tactic interpretation from Tacenv to Vernacentries.
This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions