diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/libcoqrun.clib | 4 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 32 |
2 files changed, 36 insertions, 0 deletions
diff --git a/kernel/byterun/libcoqrun.clib b/kernel/byterun/libcoqrun.clib new file mode 100644 index 0000000000..c06e408672 --- /dev/null +++ b/kernel/byterun/libcoqrun.clib @@ -0,0 +1,4 @@ +coq_fix_code.o +coq_memory.o +coq_values.o +coq_interp.o diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib new file mode 100644 index 0000000000..a628e5cfe7 --- /dev/null +++ b/kernel/kernel.mllib @@ -0,0 +1,32 @@ +Names +Univ +Esubst +Term +Mod_subst +Sign +Cbytecodes +Copcodes +Cemitcodes +Declarations +Retroknowledge +Pre_env +Cbytegen +Environ +Conv_oracle +Closure +Reduction +Type_errors +Entries +Modops +Inductive +Typeops +Indtypes +Cooking +Term_typing +Subtyping +Mod_typing +Safe_typing + +Vm +Csymtable +Vconv
\ No newline at end of file |