search

gmalecha / coq-smt-check

Invoke SMT solvers from Coq to check obligations
MIT License
10 stars 3 forks source link

Coq8.6 support? #4

Open wangjwchn opened 7 years ago

wangjwchn commented 7 years ago

Are you going to update it for Coq8.6?

gmalecha commented 7 years ago

I will look into it. I know some pieces of the Coq API changed, so I need to look into what needs to be fixed.

gmalecha commented 7 years ago

I've pushed a new branch called coq-8.6. I haven't been able to test it thoroughly yet, but if you'd like to test it out, I'd welcome feedback.

gmalecha commented 5 years ago

I'm planning on updating this to support Coq 8.9 and 8.10 in the near future (but probably not for a week or two)

wangjwchn commented 5 years ago

Great!

gmalecha commented 4 years ago

It seems like SMTCoq is a viable alternative to this repository. @wangjwchn would that address your needs?