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/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 326bf0d6ad..b9f434f179 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -116,7 +116,7 @@ let subst_const_body sub cb =
         const_body = body';
         const_type = type';
         const_body_code =
-          Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
+          Option.map (Vmemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
         const_relevance = cb.const_relevance;
         const_inline_code = cb.const_inline_code;
-- 
cgit v1.2.3