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`
---
 library/coqlib.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/coqlib.mli')

diff --git a/library/coqlib.mli b/library/coqlib.mli
index 1e3c37a9e..17c79d2e1 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -71,8 +71,8 @@ val jmeq_module_name : string list
 val datatypes_module_name : string list
 
 (** Identity  *)
-val id : constant
-val type_of_id : constant
+val id : Constant.t
+val type_of_id : Constant.t
 
 (** Natural numbers *)
 val nat_path : full_path
-- 
cgit v1.2.3