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