diff options
| author | Pierre-Marie Pédrot | 2016-03-20 23:34:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-25 13:37:03 +0100 |
| commit | c4d62e3686926c27b172636ca8b746814d13a462 (patch) | |
| tree | c7a627b0fb392e187fe0cd72ed39656d56b81504 /kernel/nativecode.mli | |
| parent | a54579dd20e04ea919f8fa887e15dd82051fa297 (diff) | |
Moving type_uconstr to Pretyping.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions