aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-13 20:13:12 +0200
committerThéo Zimmermann2020-05-13 20:13:12 +0200
commit11b1e41c2ed7b7c714bab91a70384f75efabe852 (patch)
tree36feb28bdc663020e6dab88dd142b71fb611245f /doc/plugin_tutorial
parent4bfee4ce9ad032a08e7270cf2bee24e701f7f1b6 (diff)
parent75d32b4abaeefb505d62ae201c0edc555f473396 (diff)
Merge section on Inductive types from Gallina and CIC.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions