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 acef90143..0973ca457 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -284,7 +284,7 @@ let universe_context ?names ctx =
in map, ctx
let restrict ctx vars =
- let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in
+ let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
{ ctx with uctx_local = uctx' }
type rigid =