#238 Ill-typed proof
When the type of some data changes in the editor, it can happen that the prover saves an ill-typed proof in the PR file.
This raises an assertion error when reading the proof afterward. The only way to work it around is to manually delete the proof (or the whole proof file), which needs knowledge of the Rodin internals.
To reproduce, create a fresh context with the following elements:
set: S
cst: s1, s2
axm1: s1 : S
axm2: s2 : {s1}
thm: s2 = s1
Save the file and open the proof interactively, it gets discharged by the post-tactic. Save this proof.
Then, in the context, change "S" into "T" in the set section and axiom axm1. Save the context.
If you save the proof again, the PR file will contain two copies of the predicate "s2 : {s1}", one where the constants are of type "S" and another where they are of type "T". This triggers are an java.lang.AssertionError when the tool attempts to read this file back in memory.
Important note: you have to disable auto-proving to reproduce the problem (otherwise ML gets in the way).
This is now fixed in CVS: the proof tree is always maintained type-checked, even for hypothesis actions that are not applied.
Also fixed the absence of message in the error dialog presented to the user.
Applied another fix so that old broken proofs can still be loaded, as much as possible.
Committed it to CVS.