aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-02-16 20:03:45 +0100
committerPierre-Marie Pédrot2016-03-18 18:30:22 +0100
commit13c50b98b0a294a6056d2e00a0de44cedca7af12 (patch)
tree69fde7746ae07cd4fdce9b6da3f7cffd8481ea65 /dev/base_include
parent16939df43a089ac30fec0fcf30a2f648d007cb60 (diff)
Removing dead code in Pcoq.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions