diff options
| author | Emilio Jesus Gallego Arias | 2020-04-10 03:35:27 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-03 17:24:29 +0200 |
| commit | d4081616fafe3e9fa02cef2e0102a03638f70fd6 (patch) | |
| tree | 30bb12d9cc2e2338edaf1bdec64b5aceed82bc2b /kernel/nativecode.mli | |
| parent | 3452a14b58ab88af686d3006b843bc064ab8f911 (diff) | |
[funind] Make `build_functional_principle` use a functional evar_map
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions