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, 2 insertions, 0 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 63bd247d5..312502491 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -97,6 +97,8 @@ let subst ctx = ctx.uctx_univ_variables
let ugraph ctx = ctx.uctx_universes
+let initial_graph ctx = ctx.uctx_initial_universes
+
let algebraics ctx = ctx.uctx_univ_algebraic
let constrain_variables diff ctx =