From 444a3906dc5ab468999466046d62d2551d8cb5d2 Mon Sep 17 00:00:00 2001
From: jforest
Date: Sat, 4 Jul 2009 22:08:41 +0000
Subject: repport of commit r12221

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12222 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/recdef.ml | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a96ec6a438..25e664336c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -971,9 +971,22 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       Auto.h_auto None [] (Some [])  g
 	   | _ ->
 	       incr h_num;
-	       tclTHEN
-		 (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
-		 e_assumption
+	       (observe_tac "finishing using"
+		  (
+		    tclCOMPLETE(
+		      tclFIRST[
+			tclTHEN
+			  (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+			  e_assumption;			  
+		      Eauto.eauto_with_bases
+			false
+			(true,5)
+			[delayed_force refl_equal]
+			[Auto.Hint_db.empty empty_transparent_state false]
+		      ]
+		    )
+		  )
+	       )
       		 g)
 ;
     Command.save_named opacity;
-- 
cgit v1.2.3