diff options
| author | Théo Zimmermann | 2020-04-03 15:42:47 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-03 15:42:47 +0200 |
| commit | 4c21d78932066765a75c7d25aab8bdf72ca6ab10 (patch) | |
| tree | 6ebf737d44f3e815a7d3e3f0385d38f334ed0f5c /doc/plugin_tutorial/tuto3/src | |
| parent | acefe58cd39c9a4efee632f7f92f56fb4d5285bb (diff) | |
Extract section on funind from Gallina extensions.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src')
0 files changed, 0 insertions, 0 deletions