Issue 130: Revised fin_dep_destruct to work with the new definition of Fin

sifive / Kami

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT

Apache License 2.0

197 stars 11 forks source link

Issue 130: Revised fin_dep_destruct to work with the new definition of Fin #132

Open llee454 opened 4 years ago

llee454 commented 4 years ago

I had to fix this tactic in order for proofs in StdLibKami to work.