From 48c78b719392276b2e87be5ea368c71c01f14c85 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Sep 2015 10:21:41 +0200
Subject: Fix previous merge.

---
 proofs/pfedit.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3363d0300d..5e8221b811 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -133,7 +133,7 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
-  let evd = Evd.from_env ~ctx in
+  let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   start_proof id goal_kind evd sign typ terminator;
   try
-- 
cgit v1.2.3