diff options
author | 2017-04-21 19:29:35 +0200 | |
---|---|---|
committer | 2017-04-27 21:32:00 +0200 | |
commit | 8a3cd2fe699540f1ae5a56917d0f6b951f81d731 (patch) | |
tree | a22ed219cae82f8a6824df5b51eb571c44489eef /vernac/metasyntax.ml | |
parent | 34d8de84ceb853c98bc80a0623f9afeae317d75f (diff) |
Remove unused [rec] keywords
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions