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/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index d1c7fef738..9f976b57dd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -774,7 +774,7 @@ let universe_subst evd =
   UState.subst evd.universes
 
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
-  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
-- 
cgit v1.2.3