From a002d6ef127b4f0103012c23fc5d272739649043 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 20 Apr 2000 15:51:40 +0000
Subject: Abstraction du type typed_type (un pas vers les jugements 2 niveaux)

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

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6f41a3c643..caf667dae6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1227,10 +1227,10 @@ let is_type_arity env sigma =
   srec 
 
 let is_info_type env sigma t =
-  let s = t.typ in
+  let s = level_of_type t in
   (s = Prop Pos) ||
   (s <> Prop Null && 
-   try info_arity env sigma t.body with IsType -> true)
+   try info_arity env sigma (body_of_type t) with IsType -> true)
 
 let is_info_cast_type env sigma c = 
   match c with  
-- 
cgit v1.2.3