diff options
author | Samuel Mimram <smimram@debian.org> | 2008-01-03 16:26:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-01-03 16:26:12 +0000 |
commit | 2281410e38ef99d025ea77194585a9bc019fdaa9 (patch) | |
tree | 71ba76741c3ab6b752be876565dc34b0b0138dc5 /kernel/indtypes.ml | |
parent | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff) |
Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r-- | kernel/indtypes.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 4fe90ffd..a6fd6d04 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 9633 2007-02-09 18:40:26Z herbelin $ *) +(* $Id: indtypes.ml 10297 2007-11-07 11:05:53Z barras $ *) open Util open Names @@ -29,6 +29,9 @@ let weaker_noccur_between env x nvars t = if noccur_between x nvars t' then Some t' else None +let is_constructor_head t = + isRel(fst(decompose_app t)) + (************************************************************************) (* Various well-formedness check for inductive declarations *) @@ -116,6 +119,7 @@ let is_unit constrsinfos = | _ -> false let rec infos_and_sort env t = + let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (name,c1,c2) -> let (varj,_) = infer_type env c1 in @@ -123,8 +127,8 @@ let rec infos_and_sort env t = 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 - | _ -> [] + | _ when is_constructor_head t -> [] + | _ -> anomaly "infos_and_sort: not a positive constructor" let small_unit constrsinfos = let issmall = List.for_all is_small constrsinfos |