diff options
author | jadep <jade.philipoom@gmail.com> | 2016-08-24 17:09:28 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-08-24 17:09:28 -0400 |
commit | 5de065df4799cb43aba9195bcd88a5f0479884ff (patch) | |
tree | 6a53cf8421f23b94f17cdb2440cb104ff91aeb5a /src | |
parent | fb6fd35b9cfc454b622c8bfa1364efdbf048e0df (diff) |
Moved a tactic to Util/Tactics.v
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 1 | ||||
-rw-r--r-- | src/Util/Tactics.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 0ce214bbd..7158dc22a 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -1230,7 +1230,6 @@ Section Conversion. /\ Z.of_nat i <= bitsIn limb_widthsA /\ forall n, Z.testbit (decodeB out) n = if Z_lt_dec n (Z.of_nat i) then Z.testbit (decodeA inp) n else false. - Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. Ltac subst_lia := subst_let; subst; lia. Lemma convert'_bounded_step : forall inp i out, diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index be777512c..cee2fc2a1 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -61,6 +61,8 @@ Ltac subst_evars := | [ e := ?E |- _ ] => is_evar E; subst e end. +Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. + (** destruct discriminees of [match]es in the goal *) (* Prioritize breaking apart things in the context, then things which don't need equations, then simple matches (which can be displayed |