diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 14:06:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-12 20:38:44 +0200 |
| commit | 86b9e40c2e2fd29c747a9f3ad20ebb2701210155 (patch) | |
| tree | 3ee3e5367c76a8a506be94a5d49d5d24b3ad658b /vernac/metasyntax.ml | |
| parent | 6c3fd3b8f12eb722d18b5da765bf8aec5e95ee06 (diff) | |
Adding a missing period in a notation warning.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions