Easier to use counter-examples in the Proof back-end

[AltGr]

trafficstars

When running in "Proof" mode, you can detect e.g. two conflicting exceptions.

Catala, in this case, outputs a counter-example made of the input variables of the concerned scopes (and internal variables too (!)). This is awesome, but the two actual clashing exceptions are not directly pointed out : if the case is not obvious, you'll have to extract the counter-example to put it as a test in your program, then run Catala in Interpret mode to actually trigger the clash and get the positions of the exceptions.

Just facilitating that last step would be, I think, extremely helpful. I see two ways to do this:

• improve the message so it gives code that can be copy-pasted right into the program (maybe not so easy because of internationalisation ?). For example I had a value written as `33 $' instead of '$33'
• allow the proof-backend to automatically test its counter-example inputs through the interpreter, to get back the exact error.

What do you think ?