From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Nov 2017 18:58:27 +0100
Subject: [api] Deprecate all legacy uses of Names in core.

This will allow to merge back `Names` with `API.Names`
---
 kernel/vm.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index df638acc1f..ea38ee43f6 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -59,7 +59,7 @@ val pr_stack : stack -> Pp.t
 val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
 val val_of_named : Id.t -> values
-val val_of_constant : constant -> values
+val val_of_constant : Constant.t -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
-- 
cgit v1.2.3