Skip to content

Add case_match eqn: tactic for naming hypotheses generated by case_match

Michael Sammler requested to merge ci/msammler/case_match_eqn into master

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.

Edited by Michael Sammler

Merge request reports