Add case_match eqn: tactic for naming hypotheses generated by case_match

As discussed with @robbertkrebbers. Defining the notation using "eqn:" instead of "eqn" ":" breaks the eqn: notation for destruct. I don't know if "eqn" ":" potentially breaks anything.

assigned to @msammler

added 1 commit

• c1d56990 - Add case_match eqn: tactic for naming hypotheses generated by case_match

Compare with previous version

changed the description

unassigned @msammler

Defining the notation using "eqn:" instead of "eqn" ":" breaks the eqn: notation for destruct. I don't know if "eqn" ":" potentially breaks anything.

It appears destruct allows stuff like destruct foo as eqn : Heq so having "eqn" ":" seems right.

Also a CHANGELOG entry would be nice.

added 1 commit

• 36aa322d - Add case_match eqn: tactic for naming hypotheses generated by case_match

Compare with previous version

added 7 commits

• 36aa322d...224790c8 - 6 commits from branch master
• f4902051 - Add case_match eqn: tactic for naming hypotheses generated by case_match

Compare with previous version

added 6 commits

• f4902051...ba7cf37b - 5 commits from branch master
• aaea8a28 - Add case_match eqn: tactic for naming hypotheses generated by case_match

Compare with previous version

added 1 commit

• a6f215a9 - Add case_match eqn: tactic for naming hypotheses generated by case_match

Compare with previous version

resolved all threads

merged

mentioned in commit 3897126a