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.
---
 pretyping/pretyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 30783bfad5..a69caecabe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -202,7 +202,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
        with Not_found ->
 	 try
 	   let id = try Id.of_string s with _ -> raise Not_found in
-           evd, snd (Idmap.find id names)
+           evd, snd (Id.Map.find id names)
 	 with Not_found ->
 	   if not (is_strict_universe_declarations ()) then
   	     new_univ_level_variable ?loc ~name:s univ_rigid evd
-- 
cgit v1.2.3