From b144ef5e2698932c5b2f7cdb1688a55ce4764dae Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 16:24:54 +0200
Subject: Fix after rebase...

---
 toplevel/auto_ind_decl.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 009e423e4f..8ac273c84f 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -764,16 +764,10 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-<<<<<<< HEAD
-  let ctx = Evd.empty_evar_universe_context in
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let side_eff = side_effect_of_mode mode in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
-=======
-  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal
-    (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
->>>>>>> Univs: fix environment handling in scheme building.
   in
   ([|ans|], ctx), eff
 
-- 
cgit v1.2.3