diff options
| author | Hugo Herbelin | 2018-02-20 14:35:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 14:35:54 +0100 |
| commit | 4a7d2e906c79fcae452d44ec12de8037d2843fbc (patch) | |
| tree | 8e56db27d245da82542d94b6df3eec24587a8e78 /kernel/nativecode.mli | |
| parent | aec63ba9c8f6840d98ba731640a786138d836343 (diff) | |
Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions