From e31434db0bd91d4c6b3fec8ad09b74c3613630a0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 19 Aug 2005 21:32:46 +0000
Subject: pas besoin de List.length pour savoir si une liste est vide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7306 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d80fd80758..79b048979d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1436,7 +1436,7 @@ let rename_env subst env =
 
 let is_dependent_indtype = function
   | NotInd _ -> false
-  | IsInd (_, IndType(_,realargs)) -> List.length realargs <> 0
+  | IsInd (_, IndType(_,realargs)) -> realargs <> []
 
 let prepare_initial_alias_eqn isdep tomatchl eqn =
   let (subst, pats) = 
-- 
cgit v1.2.3