diff options
| author | Pierre-Marie Pédrot | 2016-04-25 12:34:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 12:35:27 +0200 |
| commit | 76992bd0bab4d5b59e19d7a6a21c091f1c5d8340 (patch) | |
| tree | de075b506538c43a66f199f1403ea0a67536d0c1 /interp/notation.ml | |
| parent | a7917a32b24b652d2978a7aea171aa01da37eece (diff) | |
Removing dead code related to printing of ML tactics in Pptactic.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions