diff options
| author | Hugo Herbelin | 2018-05-23 18:23:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-05-23 18:50:10 +0200 |
| commit | bb2d7f94ba8688f57dc62ca72a857b82368aa784 (patch) | |
| tree | 5282ed7a0038ce0babbfc1b8b94eefa870707be8 /tactics/hints.ml | |
| parent | 33b5074f24270c202a9922f21d445c12cc6b3b3d (diff) | |
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 4eaff3fb91..3ade5314b9 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) = in if gr' == gr then gr else gr' in let subst_hint (k,data as hint) = - let k' = Option.smartmap subst_key k in - let pat' = Option.smartmap (subst_pattern subst) data.pat in + let k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (subst_pattern subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> |