aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/declare.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/declare.ml')
-rw-r--r--interp/declare.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 34bf5c8a2..bc2d2068a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -564,7 +564,7 @@ let do_universe poly l =
in
let l =
List.map (fun {CAst.v=id} ->
- let lev = Universes.new_univ_id () in
+ let lev = UnivGen.new_univ_id () in
(id, lev)) l
in
let src = if poly then BoundUniv else UnqualifiedUniv in