with the new types, even if the expansion already de-lifted the function body.
- reduceaux (tys@context) [] body'
+ reduceaux context [] body'
| C.Appl (C.CoFix (i,fl) :: tl) ->
let tys =
List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
| C.Appl (C.CoFix (i,fl) :: tl) ->
let tys =
List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
body
in
let tl' = List.map (reduceaux context []) tl in
body
in
let tl' = List.map (reduceaux context []) tl in
- reduceaux (tys@context) tl' body'
+ reduceaux context tl' body'
| t -> t
in
(match decofix (reduceaux context [] term) with
| t -> t
in
(match decofix (reduceaux context [] term) with
in
(* Possible optimization: substituting whd *)
(* recparam in l *)
in
(* Possible optimization: substituting whd *)
(* recparam in l *)
- reduceaux (tys@context) l body',
+ reduceaux context l body',
List.rev rev_constant_args
| _ -> raise AlreadySimplified
)
List.rev rev_constant_args
| _ -> raise AlreadySimplified
)
- reduceaux (tys@context) [] body'
+ reduceaux context [] body'
| C.Appl (C.CoFix (i,fl) :: tl) ->
let tys =
List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
| C.Appl (C.CoFix (i,fl) :: tl) ->
let tys =
List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
body
in
let tl' = List.map (reduceaux context []) tl in
body
in
let tl' = List.map (reduceaux context []) tl in
- reduceaux (tys@context) tl body'
+ reduceaux context tl body'
| t -> t
in
(match decofix (reduceaux context [] term) with
| t -> t
in
(match decofix (reduceaux context [] term) with