Wed, 15 Jun 2011 21:30:15 +0200 avoid compiler warning -- this is unchecked anyway;
wenzelm [Wed, 15 Jun 2011 21:30:15 +0200] rev 43406
avoid compiler warning -- this is unchecked anyway;
Wed, 15 Jun 2011 21:22:51 +0200 tuned messages;
wenzelm [Wed, 15 Jun 2011 21:22:51 +0200] rev 43405
tuned messages;
Wed, 15 Jun 2011 21:11:53 +0200 uniform use of Document_View.robust_body;
wenzelm [Wed, 15 Jun 2011 21:11:53 +0200] rev 43404
uniform use of Document_View.robust_body;
Wed, 15 Jun 2011 16:30:03 +0200 merged
wenzelm [Wed, 15 Jun 2011 16:30:03 +0200] rev 43403
merged
Wed, 15 Jun 2011 15:11:18 +0200 merge
blanchet [Wed, 15 Jun 2011 15:11:18 +0200] rev 43402
merge
Wed, 15 Jun 2011 14:36:41 +0200 fixed soundness bug made more visible by previous change
blanchet [Wed, 15 Jun 2011 14:36:41 +0200] rev 43401
fixed soundness bug made more visible by previous change
Wed, 15 Jun 2011 14:36:41 +0200 use more appropriate type systems for ATP exporter
blanchet [Wed, 15 Jun 2011 14:36:41 +0200] rev 43400
use more appropriate type systems for ATP exporter
Wed, 15 Jun 2011 14:36:41 +0200 type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases
blanchet [Wed, 15 Jun 2011 14:36:41 +0200] rev 43399
type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases
Wed, 15 Jun 2011 16:26:09 +0200 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm [Wed, 15 Jun 2011 16:26:09 +0200] rev 43398
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
Wed, 15 Jun 2011 16:22:58 +0200 more robust init;
wenzelm [Wed, 15 Jun 2011 16:22:58 +0200] rev 43397
more robust init;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip