diff options
author | 2016-05-16 15:40:27 +0200 | |
---|---|---|
committer | 2016-05-16 16:04:43 +0200 | |
commit | cead0ce54cf290016e088ee7f203d327a3eea957 (patch) | |
tree | a46bdf937ac9e4651413ddaed4be47d66300e700 /ltac/tacintern.mli | |
parent | 87f6a1684911bbd884d3f437d1d6cc5bf6f1de8f (diff) |
Generate more user-readable tactic notation kernel names.
This has no influence on user-side, and only makes the life of the debugging
developer easier.
Diffstat (limited to 'ltac/tacintern.mli')
0 files changed, 0 insertions, 0 deletions