summaryrefslogtreecommitdiff
path: root/include
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-01-08 10:30:14 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-01-08 10:30:14 -0500
commit9608c763d7b2923c11e8abd29e28271ae470a5fe (patch)
treed4648aecea89bd3799de7a6ee50a6333bd967e1a /include
parent4b109c964ac7f433b4feb9d28b135dee28f75b87 (diff)
Injected a non-special-case datatype
Diffstat (limited to 'include')
0 files changed, 0 insertions, 0 deletions