From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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/nativelambda.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 508112b35..aaa9f9b00 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -378,7 +378,7 @@ module Renv =
     type constructor_info = tag * int * int (* nparam nrealargs *)
 
     type t = {
-	name_rel : name Vect.t;
+	name_rel : Name.t Vect.t;
 	construct_tbl : constructor_info ConstrTable.t;
 
        }
-- 
cgit v1.2.3