diff options
| author | Enrico Tassi | 2014-11-03 19:06:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-11-03 19:06:28 +0100 |
| commit | 06b6a53bbc16ac2fd53213d693910c73105564c5 (patch) | |
| tree | a16da139f78ffdd9e356a971a3e8fbac3907482b /lib/xml_parser.ml | |
| parent | a30448fe3b82283e749e009a37bfd4dacb0eaaeb (diff) | |
vernac_classifier: VernacDeclareTacticDefinition does not alter the parser
Diffstat (limited to 'lib/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions