diff options
| author | Hugo Herbelin | 2020-10-31 13:23:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 16:56:49 +0100 |
| commit | 404a041fce68b4f7072de0b91b4e136f04250482 (patch) | |
| tree | da2cc1f6f2cde4839bb7796147ef9260fa4ba183 /vernac/record.ml | |
| parent | 11cb6dd5f4a719db6926ff0d99a72fbdbbf2d8bf (diff) | |
Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.
Also some dead code.
If no typo is introduced, there should be no semantic changes.
Diffstat (limited to 'vernac/record.ml')
0 files changed, 0 insertions, 0 deletions