diff options
| author | Ambroise | 2018-06-28 14:04:12 +0200 |
|---|---|---|
| committer | GitHub | 2018-06-28 14:04:12 +0200 |
| commit | f00843701373257c069d33e84b78ecaeae9e4cb0 (patch) | |
| tree | ad2fbfc6531fc58794927cf10b9fca732666a4e8 /kernel/type_errors.mli | |
| parent | 2636bf4cf12519ef1c0bf3a3a2fb2eb9194bf278 (diff) | |
Update gallina-extensions.rst
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions