From 6d998b5a0e6090b5c7d87d575016adc127b666d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 Jul 2018 18:34:06 +0200
Subject: Fix #7900 previous commit fixes a bug when using side effects in
 obligations.

Internal lemmas are inlined in obligations bodies, hence their universes
have to be declared with the obligations themselves. ~sideff:true was
not including the side effects universes and constraints in that case.
---
 engine/uState.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/uState.mli')

diff --git a/engine/uState.mli b/engine/uState.mli
index a59e61b894..f833508ebf 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -103,7 +103,7 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend: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
 
-- 
cgit v1.2.3