reduceaux context tl' body'
| t -> t
in
- (match decofix (CicReduction.whd context term) with
+ (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
with
_ -> raise AlreadySimplified
in
- (match CicReduction.whd context recparam with
+ (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
C.MutConstruct _
| C.Appl ((C.MutConstruct _)::_) ->
let body' =
| C.LetIn (_,s,t) -> aux l (S.subst s t)
| t ->
let simplified = reduceaux context l t in
- if t = simplified then
- raise AlreadySimplified
- else
- simplified
+ let t' = if l = [] then t else C.Appl (t::l) in
+ if t' = simplified then
+ raise AlreadySimplified
+ else
+ simplified
in
(try aux l body
with