CLEANUP: switching from "right-to-left" to "left-to-right" function composition operator.

Short story:

    This pull-request:

    (1) removes the definition of the "right-to-left" function composition operator

    (2) adds the definition of the "left-to-right" function composition operator

    (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead.

Long story:

    In mathematics, function composition is traditionally denoted with ∘ operator.

    Ocaml standard library does not provide analogous operator under any name.

    Batteries Included provides provides two alternatives:

    	_ % _

    and

    	_ %> _

    The first operator one corresponds to the classical ∘ operator routinely used in mathematics.
    I.e.:

    	(f4 % f3 % f2 % f1) x  ≜  (f4 ∘ f3 ∘ f2 ∘ f1) x

    We can call it "right-to-left" composition because:
    - the function we write as first (f4) will be called as last
    - and the function write as last (f1) will be called as first.

    The meaning of the second operator is this:

    	(f1 %> f2 %> f3 %> f4) x  ≜  (f4 ∘ f3 ∘ f2 ∘ f1) x

    We can call it "left-to-right" composition because:
    - the function we write as first (f1) will be called first
    - and the function we write as last (f4) will be called last
    That is, the functions are written in the same order in which we write and read them.

    I think that it makes sense to prefer the "left-to-right" variant because
    it enables us to write functions in the same order in which they will be actually called
    and it thus better fits our culture
    (we read/write from left to right).

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