aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-09 18:40:14 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-09 18:40:14 +0200
commitba50753e9da60a23a40dedea59fb7f25e3ba4d15 (patch)
tree826df6950995c06af6a9dabc5dffee96285c938c /theories/Numbers
parent8770f0db6e16aaff27a14fd48eed2ae70338f3df (diff)
No need anymore for referring to xml directory in MLINCLUDES.
Diffstat (limited to 'theories/Numbers')
0 files changed, 0 insertions, 0 deletions