diff options
| author | Hugo Herbelin | 2018-04-17 15:51:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:41:05 +0200 |
| commit | c2336868843bfe0c8e8a0b669641ca09814a45df (patch) | |
| tree | a7c72dd955484feb9217671a20d38f46571f01bc /dev | |
| parent | 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6 (diff) | |
Fixing an inconsistency in interpreting Ltac names linking to binder names.
The recursion names in fix and cofix were not renamed like other
binders were.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions