aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml/xmlcommand.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-09-02 18:26:09 +0200
committerPierre-Marie Pédrot2014-09-02 21:56:41 +0200
commit83159124ce222cb0d9811868d5a432d306c7d8f5 (patch)
tree89b762ce042cefbe55198618a16e7167ddae3c3f /plugins/xml/xmlcommand.ml
parenta50aecc7a56b7b7b1c676009f1936599366eb4ba (diff)
Fixing bug #3136.
Second-order pattern-matching now respect variable abstraction order.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions