From e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:11:22 +0200
Subject: UnivGen.extend_context -> Univ.extend_in_context_set

Such a basic function can live in Univ rather than the higher level UnivGen.
---
 kernel/univ.ml  | 3 +++
 kernel/univ.mli | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index fa37834a23..d09b54e7ec 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1065,6 +1065,9 @@ type universe_context_set = ContextSet.t
 type 'a in_universe_context = 'a * universe_context
 type 'a in_universe_context_set = 'a * universe_context_set
 
+let extend_in_context_set (a, ctx) ctx' =
+  (a, ContextSet.union ctx ctx')
+
 (** Substitutions. *)
 
 let empty_subst = LMap.empty
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1aa53b8aa8..7ac8247ca4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -433,6 +433,9 @@ end
 type 'a in_universe_context = 'a * UContext.t
 type 'a in_universe_context_set = 'a * ContextSet.t
 
+val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t ->
+  'a in_universe_context_set
+
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
-- 
cgit v1.2.3