The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Does anyone know of any work linking an SMT solver to Coq?

In particular, I'm wondering if it would be better to view multiple 
goals in Coq that are inter-dependent through shared evars as a 
satisfiability problem for the evars, or perhaps as some hybrid of 
satisfiability and proving.

Unfortunately, I don't know much about SMT, or related fields like 
constraint-based programming - just enough to think (hope?) that these 
might offer something useful to Coq with respect to solving 
evar-interdependent goals - something to supplement Coq's own 
backtracking proof search automation.

-- Jonathan