diff options
| author | Pierre-Marie Pédrot | 2014-06-30 19:01:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-30 23:14:11 +0200 |
| commit | 6987d434687890b6218b252b89b55ab5d3ef2221 (patch) | |
| tree | 0a277af5e53e525d33f044d56522651ffe1a204f /kernel/nativecode.mli | |
| parent | fa69f12babe7f04fbda9a22eaf76736a96f0fdea (diff) | |
Useless keeping of dirpath in tactic aliases.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions