diff options
| author | Pierre-Marie Pédrot | 2016-03-20 03:00:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 03:03:55 +0100 |
| commit | 25bbce0e0cb841a7ad9d5c3e7ce33711b27bf41b (patch) | |
| tree | 52f9d461a62164034bc21fed120ca8b153cf28a0 /kernel/nativevalues.ml | |
| parent | 25d49062425ee080d3e8d06920d3073e7a81b603 (diff) | |
| parent | 5f703bbb8b4f439af9d76b1f6ef24162b67049c2 (diff) | |
Moving most of Ltac code to Hightactics.
This is a major step towards the pluginification of Ltac. The one important
file that is out of reach for now is Tacsubst, as it is used in an intricate way
to handle amongst other things auto hints.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions