diff options
| author | Théo Zimmermann | 2019-12-29 20:42:55 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-29 20:42:55 +0100 |
| commit | fa94c16ca2db1d00ce05296e545ce64129b90986 (patch) | |
| tree | ca977b6ed8614a4b1717501aab27a2d394a09c06 /kernel/nativecode.mli | |
| parent | 0d359bfe1219c221aac4d29a5b443c698009ada4 (diff) | |
| parent | ae38bff8d499f4d2f82373b9c6dda1a27263d80c (diff) | |
Merge PR #11314: Convert productionlists in the Gallina chapter up to the Vernacular section to prodns
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions