Add tactic `learn_hyp`, fixes #73

This is another part of !244 (closed) and fixes #73 (closed).

added 3 commits

• 9eb7bd0f...e8ec0e0e - 2 commits from branch master
• 8cb81510 - Add [learn_hyp_named] and [learn_hyp], fixes #73 (closed)

Compare with previous version

Thanks for the MR.

• I think P is a confusing argument name of learn_hyp. The argument is a proof of a proposition, not a proposition itself.
• Can we turn these things into Tactic Notation, so that we can say learn_hyp P as H
• Can you write matches in the way we usually write them? So, a | on each line, don't use [ .. ].
• The match type of P with can simply be a let X := type_of P?

added 1 commit

• d9fe39d5 - Add [learn_hyp_named] and [learn_hyp], fixes #73 (closed)

Compare with previous version

added 8 commits

• d9fe39d5...77cb2b8a - 7 commits from branch master
• 56a9fc6b - Add [learn_hyp_named] and [learn_hyp], fixes #73 (closed)

Compare with previous version

changed title from Add [learn_hyp_named] and [learn_hyp], fixes #73 (closed) to Add {+tactic +}learn_hyp{++}, fixes #73 (closed)

@jung Any opinion, for example on the name of the tactic?

Makes sense to me, I have no ideas for a better name either.

resolved all threads

Ok, merging! Thanks @msammler

mentioned in commit 59911631

merged