diff options
| author | herbelin | 2000-04-20 15:51:40 +0000 |
|---|---|---|
| committer | herbelin | 2000-04-20 15:51:40 +0000 |
| commit | a002d6ef127b4f0103012c23fc5d272739649043 (patch) | |
| tree | 99c7ba136ce8488d2086290b3ff18fe91cdf6073 /kernel/reduction.ml | |
| parent | b8cd60cf1b3817a1802459310e79a8addb628ee7 (diff) | |
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
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |