diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ff6b33c491..077ee4e150 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -50,7 +50,7 @@ let discharge_rename_args = function (try let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in - let var_names = List.map (Name.mk_name % NamedDecl.get_id % fst) vars in + let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in let names' = List.map (fun l -> var_names @ l) names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c0a42ae7d3..a744f5ec61 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -169,7 +169,7 @@ type 'a update = | NoUpdate open Context.Named.Declaration -let inst_of_vars sign = Array.map_of_list (mkVar % get_id) sign +let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign let restrict_evar_key evd evk filter candidates = match filter, candidates with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9b44159200..af8bcb3f6d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -105,7 +105,7 @@ let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (mkVar % get_id) (named_context env.env) in + let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in let (subst, vsubst, _, nc) = Lazy.force env.extra in let typ' = subst2 subst vsubst typ in |