- match R.whd context (type_of_aux context term) with
- (*CSC manca il caso dei CAST *)
-(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
-(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
-(*CSC: Hint: nella DTD servono per gli stylesheet. *)
- C.MutInd (uri',i',exp_named_subst) as typ ->
- if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
- else raise (TypeCheckerFailure
- (NotWellTyped ("MutCase: the term is of type " ^
- CicPp.ppterm typ ^
- " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
- string_of_int i ^ "{_}")))
- | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
- if U.eq uri uri' && i = i' then
- let params,args =
- split tl (List.length tl - k)
- in params,args,exp_named_subst
- else raise (TypeCheckerFailure (NotWellTyped
- ("MutCase: the term is of type " ^
- CicPp.ppterm typ ^
- " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
- string_of_int i ^ "{_}")))
- | _ -> raise (TypeCheckerFailure
- (NotWellTyped "MutCase: the term is not an inductive one"))
+ match R.whd ~subst context (type_of_aux context term) with
+ C.MutInd (uri',i',exp_named_subst) as typ ->
+ if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
+ else raise
+ (TypeCheckerFailure
+ (sprintf
+ "Case analysys: analysed term type is %s,
+ but is expected to be (an application of) %s#1/%d{_}"
+ (CicPp.ppterm typ) (U.string_of_uri uri) i))
+ | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+ if U.eq uri uri' && i = i' then
+ let params,args =
+ split tl (List.length tl - k)
+ in params,args,exp_named_subst
+ else raise
+ (TypeCheckerFailure
+ (sprintf
+ "Case analysys: analysed term type is %s,
+ but is expected to be (an application of) %s#1/%d{_}"
+ (CicPp.ppterm typ') (U.string_of_uri uri) i))
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (sprintf
+ "Case analysis: analysed term %s is not an inductive one"
+ (CicPp.ppterm term)))