if not branches_ok then
raise
(TypeCheckerFailure "Case analysys: wrong branch type");
- let arguments =
+ let arguments' =
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) ->