From 15da5979d322c5da5f251dfd92da26407df5e45f Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 9 Oct 2002 15:42:49 +0000
Subject: retour en arriere concernant la recherche d'occurence modulo
 expansion des letins, ce qui conduisait a des comportement peu intuitifs. On
 priviligiera l'utilisation de la tactique Subst.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 483b7cfd20..f14f219229 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -49,14 +49,14 @@ let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
 
+(* Does not consider imbricated or mutually recursive types *) 
 let mis_is_recursive_subset listind rarg = 
   let rec one_is_rec rvec = 
     List.exists
       (fun ra ->
         match dest_recarg ra with
 	  | Mrec i -> List.mem i listind 
-          | Imbr _ -> array_exists one_is_rec (dest_subterms ra)
-          | Norec  -> false) rvec
+          | _ -> false) rvec
   in 
   array_exists one_is_rec (dest_subterms rarg)
 
-- 
cgit v1.2.3