if insource then
(match args with
| [arg] -> Cic.Appl (fix :: args)
- | _ -> Cic.Appl (head :: [Cic.Appl args]))
+ | _ -> Cic.Appl (fix :: [Cic.Appl args]))
else
(match args with
| [] -> head
in
(* rightno is the decreasing argument, i.e. the argument of
* inductive type *)
- Cic.Fix (0, ["f", rightno, final_ty, fixfun])
+ Cic.Fix (0, ["aux", rightno, final_ty, fixfun])
else
add_right_lambda dependent leftno (conslen + 1) 1 rightno indty
mutcase ty