aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml/xmlcommand.ml
diff options
context:
space:
mode:
authorletouzey2012-05-22 14:30:50 +0000
committerletouzey2012-05-22 14:30:50 +0000
commit78143a31a5a3f4a183b7e5a700567a51929f7fee (patch)
treee74428a5616b3fae5b607b6280c4d8253b3c962b /plugins/xml/xmlcommand.ml
parentd08282cb2242d642d8ea40e844dbe61b7404674c (diff)
Permutation: remove a compatibility notation which doesn't help MathClasses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15341 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions