+ and fix_exp_named_subst context exp_named_subst =
+ List.rev
+ (List.fold_left
+ (fun newsubst (uri,t) ->
+ let t' = eta_fix' context t in
+ let ty =
+ match CicEnvironment.get_obj uri with
+ Cic.Variable (_,_,ty,_) -> CicSubstitution.subst_vars newsubst ty
+ | _ -> raise ReferenceToNonVariable in
+ let t'' = fix_according_to_type ty t' [] in
+ (uri,t'')::newsubst
+ ) [] exp_named_subst)
+ in
+ eta_fix' context t