aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-22 14:30:50 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-22 14:30:50 +0000
commit78143a31a5a3f4a183b7e5a700567a51929f7fee (patch)
treee74428a5616b3fae5b607b6280c4d8253b3c962b /ide/minilib.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 'ide/minilib.ml')
0 files changed, 0 insertions, 0 deletions