diff options
Diffstat (limited to 'engine/uState.ml')
-rw-r--r-- | engine/uState.ml | 7 |
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 |