src/Pure/type_infer.ML
2010-09-12 wenzelm 2010-09-12 load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
2010-09-12 wenzelm 2010-09-12 common Type.appl_error, which also covers explicit constraints;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-09-12 wenzelm 2010-09-12 tuned;
2010-09-12 wenzelm 2010-09-12 tuned messages; tuned comments;
2010-06-01 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 assign now applies meet before update_new to avoid misleading error message.
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-02-06 wenzelm 2010-02-06 fixed spelling;
2009-07-23 wenzelm 2009-07-23 paramify_vars: Term_Subst.map_atypsT_same recovered coding conventions of this module;
2009-07-23 berghofe 2009-07-23 Purely functional type inference.
2009-07-17 wenzelm 2009-07-17 tuned;
2009-07-14 wenzelm 2009-07-14 tuned paramify_vars: Term_Subst.map_atypsT_option;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-06-18 wenzelm 2008-06-18 improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-09-29 wenzelm 2007-09-29 added fixate_params; type_infer: freeze_mode = NONE keeps inference parameters in result; type_infer: observe Variable.maxidx_of;
2007-09-23 wenzelm 2007-09-23 constrain: canonical argument order; removed obsolete logicT;
2007-08-31 wenzelm 2007-08-31 exported is_param;
2007-08-30 wenzelm 2007-08-30 infer_types: general check_typs instead of Type.cert_typ_mode;
2007-08-14 wenzelm 2007-08-14 infer_types: depend on Type.mode;
2007-04-23 wenzelm 2007-04-23 added paramify_vars; infer: replace params uniformly (notably freeze);
2007-04-15 wenzelm 2007-04-15 moved get_sort to sign.ML; moved decode_types to Syntax/type_ext.ML; moved mixfixT to Syntax/mixfix.ML; proper infer_types, without decode/name lookup; tuned;
2007-04-14 wenzelm 2007-04-14 tuned comment;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-27 wenzelm 2006-09-27 internal params: Vartab instead of AList;
2006-09-21 wenzelm 2006-09-21 tuned;
2006-07-19 wenzelm 2006-07-19 Name.context for used'';
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-05-05 wenzelm 2006-05-05 added syntax for _type_constraint_;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-25 wenzelm 2006-04-25 refer to structure Type instead of Sorts;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-10 wenzelm 2006-02-10 decode: observe Syntax.constN;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 tuned;
2005-12-02 wenzelm 2005-12-02 added mixfixT; paramify_dummies: treat dummyT as well, tuned;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-06 wenzelm 2005-09-06 AList.defined;
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-07-01 wenzelm 2005-07-01 avoid polyeq;
2005-06-11 wenzelm 2005-06-11 accomodate changed #classes;
2005-06-02 wenzelm 2005-06-02 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-22 wenzelm 2004-06-22 tuned certify_typ/term;
2004-06-21 wenzelm 2004-06-21 Type.cert_typ;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;
2004-05-21 wenzelm 2004-05-21 incorporate type inference interface from type.ML;
2004-05-01 wenzelm 2004-05-01 improved Term.invent_names;
2002-10-21 berghofe 2002-10-21 Replaced variantlist (quadratic) by gen_names (linear).
2002-10-07 nipkow 2002-10-07 take/drop -> splitAt
2000-03-30 wenzelm 2000-03-30 support polymorphic Vars;
2000-01-05 wenzelm 2000-01-05 support for dummy variables (anyT, logicT); improved error msg: meet *before* assign;
1999-09-29 wenzelm 1999-09-29 handle Sorts.DOMAIN;