From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 kernel/indtypes.ml | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1520e009..4fe90ffd 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
+(* $Id: indtypes.ml 9633 2007-02-09 18:40:26Z herbelin $ *)
 
 open Util
 open Names
@@ -97,19 +97,7 @@ let mind_check_arities env mie =
 
 (* Typing the arities and constructor types *)
 
-let is_info_arity env c =
-  match dest_arity env c with
-    | (_,Prop Null) -> false 
-    | (_,Prop Pos)  -> true 
-    | (_,Type _)    -> true
-
-let is_info_type env t =
-  let s = t.utj_type in
-  if s = mk_Set then true
-  else if s = mk_Prop then false
-  else
-    try is_info_arity env t.utj_val
-    with UserError _ -> true
+let is_logic_type t = (t.utj_type = mk_Prop)
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
    the product of a constructor or arity *)
@@ -132,7 +120,7 @@ let rec infos_and_sort env t =
     | Prod (name,c1,c2) ->
         let (varj,_) = infer_type env c1 in
 	let env1 = Environ.push_rel (name,None,varj.utj_val) env in
-	let logic = not (is_info_type env varj) in
+	let logic = is_logic_type varj in
 	let small = Term.is_small varj.utj_type in
 	(logic,small) :: (infos_and_sort env1 c2)
     | Cast (c,_,_) -> infos_and_sort env c
-- 
cgit v1.2.3