diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-22 22:03:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-22 22:03:41 +0100 |
| commit | c01d2f47a8202e7023250e4cfbbebdac6abb3abb (patch) | |
| tree | ef6db337c5f27d07dfa6fb0f0bb53befd7b3a278 /toplevel/vernacentries.ml | |
| parent | 4b1061a2e8cb93e6c1e3a1ef016e512eda9d0f64 (diff) | |
Announcing * and ** which were not official yet in 8.4.
Diffstat (limited to 'toplevel/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions