Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-names

The bitwise tactic was performing `intros ?m`, and the name m got
used later in many proofs. I defined a tactic notation `bitwise as m`
to be able to provide the name for `m` explicitly.

I did not make the notation local, because it seems like it would be
useful for any clients using `bitwise` who want to avoid generated
names.

I have relatively little experience with writing Ltac and tactic notations,
so if my solution can be improved, please show me how.

0 files changed, 0 insertions, 0 deletions