+ 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) -> Some (n, C.Def (E.eta_fix conjectures t))
+ ) canonical_context
+ in
+ let term' = E.eta_fix conjectures term in
+ (i,canonical_context',term')
+ ) conjectures
+ in