From 25fc4c8821140f0474735ca98d25045573e31b00 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Dec 2000 10:45:56 +0000
Subject: Suppression de la beta-iota avant appel de head_pattern_bound, ce
 sera ce dernier qui échouera si c'est pas normalisé de tête

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

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fc9c63b68e..89b16ea8a9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -202,7 +202,7 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
     | IsProd _ ->
         let ce = mk_clenv_from () (c,cty) in
 	let c' = (clenv_template_type ce).rebus in
-	let pat = Pattern.pattern_of_constr (whd_betaiota c') in
+	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
                   with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = 
-- 
cgit v1.2.3