Skip to content

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.

Edited by Michael Sammler

Merge request reports

Loading