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

4 files changed, 15 insertions, 15 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f47ab26163..04c2c51e7e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -940,8 +940,8 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl decl = Nameops.out_name (RelDecl.get_name decl)
-let var_of_decl decl = mkVar (id_of_decl decl)
+let id_of_decl = Nameops.out_name % RelDecl.get_name
+let var_of_decl = mkVar % id_of_decl
 let revert idl =
   tclTHEN
     (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
@@ -1121,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl)))
+	       prlist_with_sep spc (Ppconstr.pr_id % Nameops.out_name % RelDecl.get_name)
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl)))
+	       prlist_with_sep spc (Ppconstr.pr_id % Nameops.out_name % RelDecl.get_name)
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1279,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (fun decl -> Nameops.out_name (RelDecl.get_name decl)) princ_params))
+			  (args_id@(List.map (Nameops.out_name % RelDecl.get_name) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1558,7 +1558,7 @@ let prove_principle_for_gen
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (mkVar % Nameops.out_name % get_name) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
   let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
@@ -1586,7 +1586,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
+  let args_ids = List.map (Nameops.out_name % get_name) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | None -> error "No tcc proof !!"
@@ -1633,7 +1633,7 @@ let prove_principle_for_gen
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (fun decl -> Nameops.out_name (get_name decl))
+	(List.rev_map (Nameops.out_name % get_name)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1671,7 +1671,7 @@ let prove_principle_for_gen
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
 	 let predicates_names =
-	   List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates
+	   List.map (Nameops.out_name % get_name) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
@@ -1687,7 +1687,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (fun decl -> (Nameops.out_name (get_name decl)))
+			   (Nameops.out_name % get_name)
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1716,7 +1716,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches)
+	      (List.map (Nameops.out_name % get_name) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index d9933cf417..f8aa21e954 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -59,8 +59,8 @@ let understand = Pretyping.understand (Global.env()) Evd.empty
 let id_of_name = function
     Anonymous -> Id.of_string "H"
   | Name id   -> id;;
-let name_of_string str = Name (Id.of_string str)
-let string_of_name nme = Id.to_string (id_of_name nme)
+let name_of_string = Name.mk_name % Id.of_string
+let string_of_name = Id.to_string % id_of_name
 
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
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
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7274ac1701..80df7e48df 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -578,7 +578,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (fun decl -> out_name (RelDecl.get_name decl)) assums in
+  let params = List.map (out_name % RelDecl.get_name) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in