List.fold_right
(fun entry context ->
match entry with
- Some (name,Cic.Def t) ->
- (Some (name,Cic.Def (replace context t)))::context
+ Some (name,Cic.Def (t,None)) ->
+ (Some (name,Cic.Def ((replace context t),None)))::context
| Some (name,Cic.Decl t) ->
(Some (name,Cic.Decl (replace context t)))::context
| None -> None::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context []
else
context
List.map
(function
Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
- | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t))
+ | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context
else
context