From 86e9bba21d7a5a2d9cb092476b94f1df2370cdfa Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 6 Mar 2001 13:30:43 +0000
Subject: eta-expansion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1430 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/eauto.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index a5c27329ca..26467421fc 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -153,10 +153,9 @@ and e_my_find_search db_list local_db hdc concl =
   let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
     else 
-      list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
-	(local_db::db_list)
+      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
   in 
   let tac_of_hint = 
     fun ({pri=b; pat = p; code=t} as patac) -> 
-- 
cgit v1.2.3