From add6407b394715d29d1544ff3e59ee717601230a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 4 Jan 2009 18:26:17 +0000
Subject: Fixed bugs #2001 (search_guard was overwriting the guard index given
 by user) and #2017 (unification pattern test too crude leading to regression
 wrt to 8.1).

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

(limited to 'contrib')

diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 4079b0f200..cdbc402321 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -369,7 +369,7 @@ let solve_by_tac evi t =
     Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
     Pfedit.by (tclCOMPLETE t);
-    let _,(const,_,_) = Pfedit.cook_proof ignore in
+    let _,(const,_,_,_) = Pfedit.cook_proof ignore in
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
   with e ->
     Pfedit.delete_current_proof();
-- 
cgit v1.2.3