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
---
 proofs/proof.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 1dca04336f..35166def01 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -226,9 +226,9 @@ let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start goals =
+let start sigma goals =
   let pr = {
-    proofview = Proofview.init goals ;
+    proofview = Proofview.init sigma goals ;
     focus_stack = [] ;
     shelf = [] ;
     given_up = [] } in
-- 
cgit v1.2.3