diff options
| author | Pierre-Marie Pédrot | 2016-09-09 10:51:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-11 15:18:39 +0200 |
| commit | 5466267afa78cac5479a503338fbc57d77f05458 (patch) | |
| tree | 46d441af7085b56b88b704c14276eae7bb055bba /kernel/nativecode.ml | |
| parent | a6cd6948fa592f21b67916f423fe2adb62085492 (diff) | |
Move Ltac-specific components from G_proofs to G_ltac.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions