#3 RbP0.getPossibleApplications(): Trying to register an existing name with a different type

[Son Hoang]

In the following attachment, trying open the proof obligation thm1/S-THM for "Theory" resulting in exception "java.lang.IllegalArgumentException: Trying to register an existing name with a different type" for RbP0.getPossibleApplications().
For the user the symtom is that the operator "cmp" (which should be redden for "definition expansion") is not redden.
This is a bug reported by J-R. Abrial via email.

[Son Hoang]

The matching facilities has been reimplemented using ISpecialization which is the proper way for instantiate types in Rodin 3.x. The fix will be available in the next release of the Theory plug-in

[Guillaume Verdier]

This bug can't be reproduced with the latest version of the Theory plug-in: it is possible to open and prove thm1/S-THM without issue.
It must have been fixed at some point, but the issue was not closed at the time.