[coq] Enable backtraces on anomaly

[ejgallego]

This means we will re-execute the anomaly sentence, which may not be very safe.

Fixes #153

[ejgallego]

It seems this doesn't work, I don't know why.

Anyways this is more tricky than it looks, for example for parsing this won't work as parsing updates the input imperatively. So I guess we'd need to add a flag to eval to understand when it is safe to do so.

[ejgallego]

It seems this doesn't work, I don't know why.

I've discovered why this doesn't work, usually when we do Coq.Protect.eval ~f x , f will unfreeze the Coq state, which will set the state for anomalies back to disabled.

I guess that's hard to overcome without updating the Coq API in CDebug.

@SkySkimmer , what do you think about taking "backtraces" out of the debug flags (or even making the debug flags less synchronized)

[SkySkimmer]

IDK

[ejgallego]

We need to take a decision on this, we either patch Coq so we can do it, or close this PR.

IMHO that seems very useful, so we could try a Coq patch.

[ejgallego]

This would be possible to do using a bit of surgery on the summary, but not planned.