aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 00825208b..67479351a 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -476,6 +476,13 @@ let new_univ_variable ?loc rigid name
uctx_initial_universes = initial}
in uctx', u
+let make_with_initial_binders e us =
+ let uctx = make e in
+ List.fold_left
+ (fun uctx { CAst.loc; v = id } ->
+ fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
+ uctx us
+
let add_global_univ uctx u =
let initial =
UGraph.add_universe u true uctx.uctx_initial_universes