diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-26 17:41:34 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-26 17:41:34 -0500 |
| commit | b165133bff2fbfb713f755809b5b662a7ec2bac4 (patch) | |
| tree | b0456ab399d145f25212a3a4337acb8c773ed75c /src/Util/Tactics | |
| parent | e7a86d8ce948597934b694d8ab4d79cf586454cd (diff) | |
Rename run_tactic_as_bool to is_success_run_tactic
Diffstat (limited to 'src/Util/Tactics')
| -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 () |