Menu
▾
▴
#794 Formula factory handling during proof replay
It seems that when proofs are replayed, formulas built with different formula factories are getting mixed up. This caused some replay bugs in the Theory plug-in. They were fixed by translating the formulas in each reasoner of the plug-in, but it would be better to handle this properly in Rodin core by translating formulas to the right factory before providing them to the reasoners.
