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 /vernac/vernacentries.ml | |
| parent | d8f85f473a41037544c41d62c0ed1b70430abd14 (diff) | |
| parent | 2a628bbdd86f501b24074343653fdafa6e14c94a (diff) | |
Merge PR #7486: Update old parts of CHANGES to use current bug numbers.
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions