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

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bb4227b4a7..bd6aa09111 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1192,7 +1192,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
-  extern true (None,[]) Id.Set.empty (glob_of_pat Idset.empty env sigma pat)
+  extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
 
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
-- 
cgit v1.2.3