diff options
| author | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
| commit | 4ee0cedff7726a56ebd53125995a7ae131660b4a (patch) | |
| tree | f5049f849a27b518f5c27298058df620a0ca38b3 /kernel/kernel.mllib | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
Rename VM-related kernel/cfoo files to kernel/vmfoo
Diffstat (limited to 'kernel/kernel.mllib')
| -rw-r--r-- | kernel/kernel.mllib | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 41388d9f17..d4d7150222 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -15,9 +15,9 @@ Term CPrimitives Mod_subst Vmvalues -Cbytecodes -Copcodes -Cemitcodes +Vmbytecodes +Vmopcodes +Vmemitcodes Opaqueproof Declarations Entries @@ -30,12 +30,12 @@ Primred CClosure Relevanceops Reduction -Clambda +Vmlambda Nativelambda -Cbytegen +Vmbytegen Nativecode Nativelib -Csymtable +Vmsymtable Vm Vconv Nativeconv |