ajout des inductifs (sans types singletons pour l'instant)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@32 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7e81089453..77331bf5a2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1306,7 +1306,13 @@ let is_type_arity env =
       | _ -> false
   in 
   srec 
-    
+
+let is_info_type env t =
+  let s = t.typ in
+  (s = Prop Pos) ||
+  (s <> Prop Null && 
+   try info_arity env t.body with IsType -> true)
+
 let is_info_cast_type env c = 
   match c with  
     | DOP2(Cast,c,t) ->