From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Aug 2020 13:07:54 +0200
Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo

---
 kernel/mod_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 44b010204b..5873d1f502 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -124,8 +124,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
         { cb with
           const_body = def;
           const_universes = univs ;
-          const_body_code = Option.map Cemitcodes.from_val
-              (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
+          const_body_code = Option.map Vmemitcodes.from_val
+              (Vmbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
-- 
cgit v1.2.3