aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 30783bfad..a69caecab 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