From b165133bff2fbfb713f755809b5b662a7ec2bac4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 26 Nov 2017 17:41:34 -0500 Subject: Rename run_tactic_as_bool to is_success_run_tactic As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144 --- src/Util/Tactics/RunTacticAsConstr.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/Tactics') 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 () -- cgit v1.2.3