diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-17 10:32:40 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-17 11:13:04 +0100 |
| commit | 06fa0334047a9400d0b5a144601fca35746a53b8 (patch) | |
| tree | c3afdf28353d5ea096b1c6e3aece87ed17015b1c /proofs/tacmach.ml | |
| parent | 9a7afc12e0573c74d0bb0943372dddc3c61a03f1 (diff) | |
CLEANUP: Renaming "Util.compose" function to "%"
I propose to change the name of the "Util.compose" function to "%".
Reasons:
1. If one wants to express function composition,
then the new name enables us to achieve this goal easier.
2. In "Batteries Included" they had made the same choice.
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a10d8fd2f..1e59c182c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -99,7 +99,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv |