From 2e03ae95b48638c01d66ecced32a4f5ae24a3e6e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 23:46:04 +0000
Subject: Normalisation betaiota du pattern avant enregistrement comme hint
 (certains développements exploite cette caractéristique)

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

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