diff options
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 |