From d71f9b16a49ce4faa61ba9b3c57f43c3acceb8cb Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 4 Nov 2013 13:20:47 +0000
Subject: Allowing proofs starting with a non-empty evarmap.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/leminv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 86ec3a8357..106205552d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -196,7 +196,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start [invEnv,invGoal] in
+  let pf = Proof.start Evd.empty [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf)
-- 
cgit v1.2.3