diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-30 19:01:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-30 23:14:11 +0200 |
| commit | 6987d434687890b6218b252b89b55ab5d3ef2221 (patch) | |
| tree | 0a277af5e53e525d33f044d56522651ffe1a204f /toplevel/mltop.ml | |
| parent | fa69f12babe7f04fbda9a22eaf76736a96f0fdea (diff) | |
Useless keeping of dirpath in tactic aliases.
Diffstat (limited to 'toplevel/mltop.ml')
0 files changed, 0 insertions, 0 deletions