diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:23:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:50:10 +0200 |
| commit | bb2d7f94ba8688f57dc62ca72a857b82368aa784 (patch) | |
| tree | 5282ed7a0038ce0babbfc1b8b94eefa870707be8 /pretyping/glob_ops.ml | |
| parent | 33b5074f24270c202a9922f21d445c12cc6b3b3d (diff) | |
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 102e89400..5056c0457 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -343,7 +343,7 @@ let map_inpattern_binders f ({loc;v=(id,nal)} as x) = else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = - let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in + let r = Option.Smart.map (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) |