EclecticLib.v --> Tactic failure: resersible in 1st order mode

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

EclecticLib.v --> Tactic failure: resersible in 1st order mode #135

Open nanoeng opened 2 years ago

nanoeng commented 2 years ago

Howdy,

Every time I try to compile the current EclecticLib.v using the CoqIDE compiler, the following error messages show up

795: Tactic failure: reversible in 1st order mode.
800: Tactic failure: reversible in 1st order mode.
893: [Focus] Wrong bullet +: Current bullet + is not finished.
904: The reference h was not found in the current environment.

Would appreciate it if you guys could please let me know if I'm missing anything.

Thanks in advance!