Backtrack on making exact hints for lemmas starting with products

(e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of
useless eta-redexes during type class instance resolution.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 7 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b6dc4e598c..6a08bda87a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -270,13 +270,16 @@ let dummy_goal =
 
 let make_exact_entry pri (c,cty) =
   let cty = strip_outer_cast cty in
-  let pat = Pattern.pattern_of_constr cty in
-  let head = 
-    try head_of_constr_reference (fst (head_constr cty)) 
-    with _ -> failwith "make_exact_entry" 
-  in
-    (Some head,
-    { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
+    match kind_of_term cty with
+    | Prod _ -> failwith "make_exact_entry"
+    | _ ->
+	let pat = Pattern.pattern_of_constr cty in
+	let head = 
+	  try head_of_constr_reference (fst (head_constr cty)) 
+	  with _ -> failwith "make_exact_entry" 
+	in
+          (Some head,
+	  { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
   let cty = if hnf then hnf_constr env sigma cty else cty in