- | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true
- (* TASSI: da verificare *)
- | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
- let res = CicReduction.are_convertible context so ind
- in
- res &&
- (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop -> true
- | (C.Sort C.Set | C.Sort C.CProp) ->
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- (* is a singleton definition? *)
- List.length cl = 1
- | _ ->
- raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))
- )
- | _ -> false
- )
- | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
- when not need_dummy ->
- let res = CicReduction.are_convertible context so ind
- in
- res &&
- (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop
- | C.Sort C.Set -> true
- | C.Sort C.CProp -> true
- | C.Sort (C.Type _) ->
- (* TASSI: da verificare *)
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,paramsno) ->
- let (_,_,_,cl) = List.nth itl i in
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
- in
- List.fold_right
- (fun (_,x) i -> i && is_small ~logger tys paramsno x) cl true
- | _ ->
- raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))
- )
- | _ -> raise (AssertFailure "19")
- )
- | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
- (* TASSI: da verificare *)
- CicReduction.are_convertible context so ind
- | (_,_) -> false
-
-and type_of_branch context argsno need_dummy outtype term constype =