It looks like this option is known to be broken. Maybe it's better to remove it (as an user-facing setting), or at least add in the description that is has known problems?
There's this reported issue, where the comment says that this option is known to be broken:
#940
I've also had a problem with it:
#Rocq users > ✔ Qed "Attempt to save an incomplete proof"
It looks like this option is known to be broken. Maybe it's better to remove it (as an user-facing setting), or at least add in the description that is has known problems?
There's this reported issue, where the comment says that this option is known to be broken:
#940
I've also had a problem with it:
#Rocq users > ✔ Qed "Attempt to save an incomplete proof"