+ let conjectures' =
+ List.map
+ (function (i,canonical_context,term) ->
+ let canonical_context' =
+ List.map
+ (function
+ None -> None
+ | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
+ | Some (n, C.Def (t,None)) ->
+ Some (n, C.Def ((E.eta_fix conjectures t),None))
+ | Some (_,C.Def (_,Some _)) -> assert false
+ ) canonical_context
+ in
+ let term' = E.eta_fix conjectures term in
+ (i,canonical_context',term')
+ ) conjectures
+ in