From e705297921639fa0aef7d6e50e58d50257de3160 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Aug 2018 09:35:21 +0200
Subject: Fix #7795: UGraph.AlreadyDeclared with Program

This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
---
 proofs/pfedit.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 678c3ea3f7..b48f14ca82 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -173,8 +173,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
       const_entry_body = Future.chain ce.const_entry_body
         (fun (pt, _) -> pt, ()) } in
   let (cb, ctx), () = Future.force ce.const_entry_body in
-  let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  cb, status, Evd.evar_universe_context univs'
+  let univs = UState.merge side_eff Evd.univ_rigid univs ctx in
+  cb, status, univs
 
 let refine_by_tactic env sigma ty tac =
   (** Save the initial side-effects to restore them afterwards. We set the
-- 
cgit v1.2.3