Wed, 28 Apr 2010 11:09:19 +0200modernized/simplified Sign.set_defsort;
wenzelm [Wed, 28 Apr 2010 11:09:19 +0200] rev 36449
modernized/simplified Sign.set_defsort;

Wed, 28 Apr 2010 10:51:34 +0200get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
wenzelm [Wed, 28 Apr 2010 10:51:34 +0200] rev 36448
get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
tuned;

Wed, 28 Apr 2010 10:43:08 +0200export Type.minimize_sort;
wenzelm [Wed, 28 Apr 2010 10:43:08 +0200] rev 36447
export Type.minimize_sort;

Wed, 28 Apr 2010 08:25:02 +0200term_typ: print styled term
haftmann [Wed, 28 Apr 2010 08:25:02 +0200] rev 36446
term_typ: print styled term

Tue, 27 Apr 2010 22:23:12 +0200merged
wenzelm [Tue, 27 Apr 2010 22:23:12 +0200] rev 36445
merged

Tue, 27 Apr 2010 21:53:55 +0200removed obsolete sanity check -- Sign.certify_sort is stable;
wenzelm [Tue, 27 Apr 2010 21:53:55 +0200] rev 36444
removed obsolete sanity check -- Sign.certify_sort is stable;

Tue, 27 Apr 2010 21:46:10 +0200monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
wenzelm [Tue, 27 Apr 2010 21:46:10 +0200] rev 36443
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;

Tue, 27 Apr 2010 21:34:22 +0200really minimize sorts after certification -- looks like this is intended here;
wenzelm [Tue, 27 Apr 2010 21:34:22 +0200] rev 36442
really minimize sorts after certification -- looks like this is intended here;

Tue, 27 Apr 2010 19:44:04 +0200tuned signature;
wenzelm [Tue, 27 Apr 2010 19:44:04 +0200] rev 36441
tuned signature;

Tue, 27 Apr 2010 11:17:50 -0700merged
huffman [Tue, 27 Apr 2010 11:17:50 -0700] rev 36440
merged