diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 15:40:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 16:04:43 +0200 |
| commit | cead0ce54cf290016e088ee7f203d327a3eea957 (patch) | |
| tree | a46bdf937ac9e4651413ddaed4be47d66300e700 /ltac/tacsubst.ml | |
| 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/tacsubst.ml')
0 files changed, 0 insertions, 0 deletions