diff options
| author | Pierre-Marie Pédrot | 2013-12-02 17:16:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-02 17:16:04 +0100 |
| commit | 9d8c2060a64f77a7d3a86bb8cd2631c5819cf553 (patch) | |
| tree | 23b54be4e8313ce533800d5e0ff987cddee75d5e /plugins/xml/xmlcommand.ml | |
| parent | 85ed2504568ee06207546b1ac0660e9c559bca22 (diff) | |
Porting type interpretation in Tacinterp to the new tactics.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions