src/Pure/type_infer_context.ML
Tue, 03 Apr 2012 16:10:34 +0200 wenzelm better drop background syntax if entity depends on parameters;
Mon, 12 Mar 2012 13:53:26 +0100 wenzelm clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
Thu, 10 Nov 2011 22:32:10 +0100 wenzelm pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
Wed, 09 Nov 2011 20:47:11 +0100 wenzelm tuned signature;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Tue, 19 Apr 2011 20:47:02 +0200 wenzelm split Type_Infer into early and late part, after Proof_Context;
less more (0) tip