diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 14:57:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 15:19:06 +0200 |
| commit | dfa99b152114271cf9fac4cab9d8663ac6ec078c (patch) | |
| tree | 80e8af6b339a263580cf1ad4c70c0e3269b4f89c /vernac/metasyntax.ml | |
| parent | e559f7553030dc3a86936794d0f80f39b0131960 (diff) | |
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions