diff options
| author | Hugo Herbelin | 2016-04-13 21:17:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:47 +0200 |
| commit | ee882d4cf6e7d84dc4589535042bbefdec56a288 (patch) | |
| tree | 20d46dbf2b45bfad53af2a9873839cd4d67befab /plugins/syntax/string_syntax.ml | |
| parent | 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc (diff) | |
Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.
No other changes (long only because of a change of indentation).
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions