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 /tactics/autorewrite.ml | |
| parent | 33b5074f24270c202a9922f21d445c12cc6b3b3d (diff) | |
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 627ac31f5..0b0e629ab 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -30,7 +30,7 @@ let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in + let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; |