diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-04 20:59:28 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-04 20:59:28 +0200 |
commit | b0ed0c2c1c7ca8fc434ecadd3a9ed906e6e428c2 (patch) | |
tree | 877b7cf28198b4441282cb860646aed99124fdae /plugins/ltac/tacarg.ml | |
parent | d8f85f473a41037544c41d62c0ed1b70430abd14 (diff) | |
parent | 2a628bbdd86f501b24074343653fdafa6e14c94a (diff) |
Merge PR #7486: Update old parts of CHANGES to use current bug numbers.
Diffstat (limited to 'plugins/ltac/tacarg.ml')
0 files changed, 0 insertions, 0 deletions