+ 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 =
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o 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