From 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Sep 2015 18:35:48 +0200
Subject: Univs: Add universe binding lists to definitions

... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
---
 proofs/pfedit.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d024c01ba5..c77ab06b94 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 Environ.empty_env in
+  let evd = Evd.from_ctx ctx in
   start_proof id goal_kind evd sign typ (fun _ -> ());
   try
     let status = by tac in
-- 
cgit v1.2.3