diff options
| author | Hugo Herbelin | 2019-11-12 09:32:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 20:45:22 +0100 |
| commit | e7b29adca3c2ff636ff277dab843d517894f3bf6 (patch) | |
| tree | bad5adadc9fd93f6bfdd1c826538162478486713 /kernel/nativecode.mli | |
| parent | d10e7cc978a2abd97377c6365cc5366cf5cdf5eb (diff) | |
Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions