diff options
| author | Matej Kosik | 2016-08-29 15:35:45 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-08-29 15:56:18 +0200 |
| commit | e969a56e2d0c354057b4d9da0d48349d2a5a61e2 (patch) | |
| tree | a34ce5ef80fd65ec874d265a3dc48ccd0b75743c /pretyping | |
| parent | 2c513c07473b40c390dc1e1d24bfaf971c685514 (diff) | |
CLEANUP: taking advantage of "_ % _" operator to express function composition in a more obvious way
This commit rewrites terms
(fun x -> f1 (f2 ... (fN x)...))
to
f1 % f2 % ... % fN
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0f85dc629c..f044e919b5 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 (fun d -> mkVar (get_id d)) (named_context env.env) in + let inst_vars = List.map (mkVar % get_id) (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 |