aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorHugo Herbelin2014-11-10 12:36:02 +0100
committerHugo Herbelin2014-11-22 19:23:32 +0100
commit95e6ce19d4f05a51b76c3305e52170a6c933f4a4 (patch)
tree98ddbd3e1c656b0e8a2848d02efe3bcf103cea8f /dev/include
parentf3bc425bdf6274e646b94dc0c7d157b9c845be43 (diff)
Further simplifying functional induction.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions