diff options
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) |