From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 4 Nov 2017 18:14:38 +0100
Subject: [api] Deprecate all legacy uses of Name.Id in core.

This is a first step towards some of the solutions proposed in #6008.
---
 library/globnames.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/globnames.ml')

diff --git a/library/globnames.ml b/library/globnames.ml
index dc9541a0d..5c75994dd 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -84,7 +84,7 @@ let is_global c t =
   | ConstRef c, Const (c', _) -> eq_constant c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
-  | VarRef id, Var id' -> id_eq id id'
+  | VarRef id, Var id' -> Id.equal id id'
   | _ -> false
 
 let printable_constr_of_global = function
-- 
cgit v1.2.3