From ea41376804c30a583377c0ca45ad8e1b378838df Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 16 Jul 2002 10:34:31 +0000
Subject: un cas inutile dans un pattern matching

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

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2380b94c82..35c6a2370a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -84,7 +84,7 @@ let typeur sigma metamap =
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Cast (c,t) -> t
-    | Sort _ | Prod (_,_,_) | Ind _ -> mkSort (sort_of env cstr)
+    | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
   and sort_of env t = 
     match kind_of_term t with
-- 
cgit v1.2.3