Initing a REPL using segment init inside a proof causes problems
after finishing the proof. The 'finish' closure seems to be gone,
meaning the finished proof is not recorded - i.e. not available under the name the proof
was started with. Furthermore, when it concerns a proof in a locale, qed seems to throw
you out of that locale, causing different problems down the line.
Small reproducer available here: 2f2f6fb
Initing a REPL using segment init inside a proof causes problems
after finishing the proof. The '
finish' closure seems to be gone,meaning the finished proof is not recorded - i.e. not available under the name the proof
was started with. Furthermore, when it concerns a proof in a locale,
qedseems to throwyou out of that locale, causing different problems down the line.
Small reproducer available here: 2f2f6fb