From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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.
---
 engine/evarutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index eabfb7b398..38efcca050 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -306,7 +306,7 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
   in
   let extract_if_neq id = function
     | Anonymous -> None
-    | Name id' when id_ord id id' = 0 -> None
+    | Name id' when Id.compare id id' = 0 -> None
     | Name id' -> Some id'
   in
   let na = RelDecl.get_name decl in
-- 
cgit v1.2.3