aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 1dd8acd0d..6c8dbe3f4 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -296,7 +296,7 @@ let constrain_variables diff ctx =
let reference_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname)
+ try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
with Not_found | Option.IsNone ->
Universes.reference_of_level l