aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml/xmlcommand.mli
diff options
context:
space:
mode:
authorsoubiran2010-04-16 14:14:28 +0000
committersoubiran2010-04-16 14:14:28 +0000
commit456ff087953a62df0b46e76f16d0117363558b0d (patch)
tree2cec913f9689e6410c0ecebe3d95b076464cd942 /plugins/xml/xmlcommand.mli
parentd31d8723b5b103b4937c63dd2560c07b04492a3a (diff)
cf. 12945
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12946 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.mli')
0 files changed, 0 insertions, 0 deletions