aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 282acb3d6e..ff91493ee5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -315,6 +315,9 @@ let check_univ_decl uctx decl =
ctx
let restrict ctx vars =
+ let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
+ (fst ctx.uctx_names) vars
+ in
let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
{ ctx with uctx_local = uctx' }