diff options
| author | Théo Zimmermann | 2019-05-24 16:36:46 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-24 16:36:46 +0200 |
| commit | 5727443376480be4793757fd5507621ad4f09509 (patch) | |
| tree | 2fff9e86c24d1d6d82c3ed59919d3b3de4112189 /lib | |
| parent | 5596cf352d1c265fd5627dc19416d2b55c10f2b7 (diff) | |
| parent | be40007de49140d403bb1dad1af9f4f1e3fe5003 (diff) | |
Merge PR #10233: Fixing typos - Part 3
Reviewed-by: Zimmi48
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | lib/util.ml | 2 | ||||
| -rw-r--r-- | lib/util.mli | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 8b3a07d4b2..bc20a66824 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -18,7 +18,7 @@ (* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned against its use, *) +(* uses, however regular users are _strongly_ warned against its use, *) (* they should instead rely on the available functions below. *) (* *) (* Box order and number is indeed an important factor. Try to create *) diff --git a/lib/util.ml b/lib/util.ml index 38d73d3453..6e8b8de5dc 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -14,7 +14,7 @@ let on_fst f (a,b) = (f a,b) let on_snd f (a,b) = (a,f b) let map_pair f (a,b) = (f a,f b) -(* Mapping under pairs *) +(* Mapping under triplets *) let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) diff --git a/lib/util.mli b/lib/util.mli index 1eb60f509a..9a00ee3440 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,7 +17,7 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Mapping under triple *) +(** Mapping under triplets *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd |