I have some complex functional code in Gallina that I run under Coq. From time to time bugs emerge and I need to debug the code. Is there a way to debug the code from Coq, or am I stuck with doing everything by hand?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
There is a plugin which allows to do prints from gallina functions:
https://github.com/coq-community/reduction-effects
I find this quite effective for debugging gallina code.
