search

vafeiadis / hahn

Hahn: A Coq library
MIT License
29 stars 15 forks source link

des* tactics: destruct H -> generalize H; clear H; intros [] #13

Closed anlun closed 4 years ago

anlun commented 4 years ago

I tried to address #12, however, the fix breaks the project compilation for a unknown reason on l.216 of HahnTotalList.v.

vafeiadis commented 4 years ago

Instead fixed by a0cbf4c77971027dc170a7c961ef8f8773741353 commit.