diff options
| author | Pierre-Marie Pédrot | 2015-01-21 00:26:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-21 00:46:06 +0100 |
| commit | c2d053c6f38a54e3083c8726eccb3e73942107b7 (patch) | |
| tree | 2eef9978ece47590799ab97acfe9043e213b8d40 /kernel/nativecode.ml | |
| parent | 9cc95f5a34b9050fe5a869f0fb96da562b45353d (diff) | |
Embedding the index of the ML tactic entry in the Tacexpr AST.
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions