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

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7609c1a64d..9c32cd8e0e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -107,7 +107,7 @@ type 'opaque constant_body = {
     const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
     const_type : types;
     const_relevance : Sorts.relevance;
-    const_body_code : Cemitcodes.to_patch_substituted option;
+    const_body_code : Vmemitcodes.to_patch_substituted option;
     const_universes : universes;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
-- 
cgit v1.2.3