diff options
Diffstat (limited to 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8410e08ccd..d1d3d90c5c 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -22,7 +22,7 @@ open Misctypes (* Basic tactics *) let h_intro_move x y = abstract_tactic (TacIntroMove (x, y)) (intro_move x y) -let h_intro x = h_intro_move (Some x) no_move +let h_intro x = h_intro_move (Some x) MoveLast let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption let h_exact c = abstract_tactic (TacExact c) (exact_check c) |