From f1874a538ef7e5886b72c2ec2ce21b23d05aa8d7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 30 Aug 1999 13:17:26 +0000
Subject: 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
---
 kernel/reduction.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel/reduction.ml')

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) -> 
-- 
cgit v1.2.3