an application with no arguments was created.
if not branches_ok then
raise
(TypeCheckerFailure "Case analysys: wrong branch type");
if not branches_ok then
raise
(TypeCheckerFailure "Case analysys: wrong branch type");
if not need_dummy then outtype::arguments@[term]
else outtype::arguments in
let outtype =
if not need_dummy then outtype::arguments@[term]
else outtype::arguments in
let outtype =
- if arguments = [] then outtype
- else CicReduction.head_beta_reduce (C.Appl arguments)
+ if need_dummy && arguments = [] then outtype
+ else CicReduction.head_beta_reduce (C.Appl arguments')
in
outtype,ugraph5
| C.Fix (i,fl) ->
in
outtype,ugraph5
| C.Fix (i,fl) ->