From 56a6727525e860a155b6ae73da152e558b3ea976 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Aug 2014 15:51:21 +0200
Subject: Cleaning up interface of ContextSet.

Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
---
 pretyping/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c60fb29586..c5657cc52d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -989,7 +989,7 @@ let with_context_set rigid d (a, ctx) =
 let uctx_new_univ_variable rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
-  let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in
+  let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx' = 
     match rigid with
     | UnivRigid -> uctx
-- 
cgit v1.2.3