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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/univ.mli')

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