diff options
| author | Pierre-Marie Pédrot | 2014-05-16 16:41:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-16 16:41:29 +0200 |
| commit | c2f78ed4fba9fa027fdf2051f214e1c5b4fe670e (patch) | |
| tree | 42f41ae796eb1051bc9735f4f3dd95b51a192091 /kernel | |
| parent | 7491ffa371ab7537dd4d7b85af1079a792dd6e96 (diff) | |
Slightly better printer for native ML tactics, in order to disambiguate
them.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions