From ed54c8c767c6a3dfe9ce453c57bd849c20df7951 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Feb 2007 18:42:56 +0000
Subject: Suppresion de la catégorie des inductifs singletons larges dont
 l'élimination vers Set était autorisée: comme souligné par Benjamin, c'est
 incompatible avec EM + AC (report rev 9633 8.1)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 11264a9e38..e8f9dbc326 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -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