From 2281410e38ef99d025ea77194585a9bc019fdaa9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 3 Jan 2008 16:26:12 +0000 Subject: Imported Upstream version 8.1.pl3+dfsg --- kernel/indtypes.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'kernel/indtypes.ml') 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 -- cgit v1.2.3