diff options
| author | Pierre-Marie Pédrot | 2014-08-09 15:51:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-09 15:59:01 +0200 |
| commit | 56a6727525e860a155b6ae73da152e558b3ea976 (patch) | |
| tree | d4a2c5e3d64fb5c7bbb409f6c89c61dd23b174b6 /pretyping | |
| parent | eec72af81a84f7b56b04027693684eebe139a607 (diff) | |
Cleaning up interface of ContextSet.
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |