| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-02-26 | Delay the dynamic linking of native-code libraries until native_compute is ↵ | Guillaume Melquiond | |
| called (fix #13849). The libraries are eventually linked in native_norm and native_conv_gen, just before mk_norm_code and mk_conv_code are called. This commit also renames call_linker as execute_library to better reflect its role. It also makes link_library independent from it, since their error handling are completely opposite. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |