Unique names for goals

[jldodds]

A common idiom for debugging failing proofs is to print the goal in a tactic prior to proving it. Currently, a goal will be made up of multiple goals, some of which might share a name, e.g.
Goal s2n_hmac_init (safety assertion: literal equality postcondition). Looking at the proof term, it then takes additional effort to discover which goal has failed.

Possible solutions that would make this workflow easier include

• Number all goals
• Provide SAW line numbers the goals were created on in the name
• Provide a tactic that prints or returns the goal that failed

[brianhuffman]

We already number saw-core proof goals. We should just make sure to always print out the goal number along with the name.

[RyanGlScott]

print_goal now prints out the goal number as of 2e494e4. I'll going and close this, but feel free to reopen if there is something else remaining to be done.