diff options
| author | Jason Gross | 2017-04-28 14:02:00 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-04-28 14:02:00 -0400 |
| commit | 6deddd3e0c6cc1d7cbf8414f7553c5d7752a0801 (patch) | |
| tree | 1eab4605d82535a40a93ba7ef9db69feb7246174 /kernel/nativecode.mli | |
| parent | 7943b1fade775af48917d54878e65b80217be038 (diff) | |
Allow interactive editing of {C,}Morphisms in PG
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions