diff options
| -rw-r--r-- | src/Util/Tactics/RunTacticAsConstr.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Tactics/RunTacticAsConstr.v b/src/Util/Tactics/RunTacticAsConstr.v index d3d5ee096..cd96ebcd2 100644 --- a/src/Util/Tactics/RunTacticAsConstr.v +++ b/src/Util/Tactics/RunTacticAsConstr.v @@ -6,7 +6,7 @@ Ltac run_tactic tac := I. (** Runs a tactic during expression evaluation phase, returning [true] on success and [false] on failure. *) -Ltac run_tactic_as_bool tac := +Ltac is_success_run_tactic tac := match goal with | _ => let dummy := run_tactic tac in true @@ -16,7 +16,7 @@ Ltac run_tactic_as_bool tac := (** Runs a tactic during expression evaluation phase; on success, returns [then_tac ()], otherwise returns [else_tac ()] *) Ltac constr_tryif_then_else tac then_tac else_tac := - let success := run_tactic_as_bool tac in + let success := is_success_run_tactic tac in lazymatch success with | true => then_tac () | false => else_tac () |