From 3d977093338d95950b09c1fac2bd90f48c1fd4ab Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 16 Oct 2019 21:19:39 +0200
Subject: re-expose UState.demote_seff_univs

provide minimal functionality for https://github.com/mit-plv/rewriter
plugin (declaring inductives as side effects, so there's no private
constant to use with emit_side_effects)
---
 engine/uState.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine/uState.mli')

diff --git a/engine/uState.mli b/engine/uState.mli
index 7cb2f49780..23ef84c55d 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -112,6 +112,11 @@ val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
 val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
+val demote_seff_univs : Univ.LSet.t -> t -> t
+(** Mark the universes as not local any more, because they have been
+   globally declared by some side effect. You should be using
+   emit_side_effects instead. *)
+
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t
 
-- 
cgit v1.2.3