diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 97aeedc6b..1c0e04276 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -80,7 +80,7 @@ END TACTIC EXTEND replace | ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] -> - [ new_replace c1 c2 in_hyp (Util.option_app Tacinterp.eval_tactic tac) ] + [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ] END (* Julien: |