aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-16 16:41:29 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-16 16:41:29 +0200
commitc2f78ed4fba9fa027fdf2051f214e1c5b4fe670e (patch)
tree42f41ae796eb1051bc9735f4f3dd95b51a192091 /theories
parent7491ffa371ab7537dd4d7b85af1079a792dd6e96 (diff)
Slightly better printer for native ML tactics, in order to disambiguate
them.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions