diff options
| author | Théo Zimmermann | 2018-07-02 19:04:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-02 19:04:18 +0200 |
| commit | 0a556686f5c759e61dc740dd1b2762a077a19f40 (patch) | |
| tree | 68cb03e948f69babc5a9ca2e76b73cb46d8c3d66 /kernel/nativecode.mli | |
| parent | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (diff) | |
| parent | 905770ed2a8b9b760b9a8c1384d4d65cdb82892e (diff) | |
Merge PR #7965: doc: Fix typesetting in Gallina extensions
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions