Son Hoang

Resotore removeFeature.xml

Remove EMF Inclusions and CamilleX (now available from Soton update site)

Removed eXtended Event-B editors (now CamilleX)

Move scripts for setting up composite update site to a folder

We will need another release of Rodin when Eclipse 2020-12 is released.

Refreshing issue on Mac OS X Big Sur 11.0.0

I now remember that it is about proof reuse. In order to reuse the proofs, the number of sub-goals has to be identical. This decision has been made since the early development of Rodin, i.e., the constraints is that every reasoner with the same input will produce the same number of sub-goal. For example, if you change your operator so that the WD is not longer trivial, the shape of your proof tree changed, hence you potentially lose all the sub-proofs. So this is a feature, not a bug.

I cannot remember the exact reason, but it must have something to do with Well-definedness.