Prise en compte des let-in dans les fonctions de réduction pour les tactiques

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

1 files changed, 2 insertions, 2 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 018197dd49..c1edbafafd 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -247,14 +247,14 @@ let reduce_to_ind_goal gl t =
     match kind_of_term c with
       | IsMutInd (ind_sp,args as ity) -> 
 	  ((ity, path_of_inductive_path ind_sp, t), t)
-      | IsConst _ ->
-	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t))
       | IsCast (c,_) when args = [] ->
 	  elimrec c
       | IsProd (n,ty,t') when args = [] ->
 	  let (ind, t) = elimrec t' in (ind, mkProd (n,ty,t))
       | IsLetIn (n,c,ty,t') when args = [] ->
 	  let (ind, t) = elimrec t' in (ind, mkLetIn (n,c,ty,t))
+      | _ when Instantiate.isEvalRef c ->
+	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t))
       | _ -> error "Not an inductive product"
   in 
   elimrec t