Hi Florian,
I'm investigating a regression which prevents identifying certain equivalent
locales through circular sublocale declarations:
sublocale loc1 < x: loc2 A c (* sigma_1 *)
where "x.b == B" and "x.d == e" (* tau_1 *)
sorry
sublocale loc2 < x: loc1 A b (* sigma_2 *)
where "
Makarius,
I have the impression that your push has not made it to the official afp-code. At least, I
cannot see it on
http://sourceforge.net/p/afp/code/ci/6ff9a8c6405d04f28365434a0e7bd65ea89aad86/log/
although my commits do show up there.
Andreas
On 10/02/15 23:08, Makarius wrote:
On Tue,