From 900bd7c4d4d6327b5ed77cb8a7cefefa749f13e3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 10:34:07 +0000
Subject: 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
---
 tactics/tacticals.ml | 4 ++--
 1 file 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
-- 
cgit v1.2.3