src/Pure/type_infer.ML
Thu, 03 Jan 2019 14:12:44 +0100 wenzelm clarified signature: more types;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Mon, 16 Sep 2013 23:04:13 +0200 wenzelm removed dead code (see also 69d4543811d0);
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Tue, 19 Apr 2011 20:47:02 +0200 wenzelm split Type_Infer into early and late part, after Proof_Context;
Tue, 19 Apr 2011 10:37:38 +0200 wenzelm more precise treatment of existing type inference parameters;
Mon, 18 Apr 2011 12:11:58 +0200 wenzelm tuned;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Mon, 28 Mar 2011 22:44:14 +0200 wenzelm address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;
Fri, 29 Oct 2010 22:54:54 +0200 wenzelm more sharing of operations, without aliases;
Mon, 13 Sep 2010 13:20:18 +0200 wenzelm tuned signature;
Mon, 13 Sep 2010 12:42:08 +0200 wenzelm Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
Mon, 13 Sep 2010 11:35:55 +0200 wenzelm simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
Sun, 12 Sep 2010 22:28:59 +0200 wenzelm Type_Infer.preterm: eliminated separate Constraint;
Sun, 12 Sep 2010 21:24:23 +0200 wenzelm Type_Infer.infer_types: plain error instead of kernel exception TYPE;
Sun, 12 Sep 2010 20:47:47 +0200 wenzelm load type_infer.ML later -- proper context for Type_Infer.infer_types;
Sun, 12 Sep 2010 19:55:45 +0200 wenzelm common Type.appl_error, which also covers explicit constraints;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Sun, 12 Sep 2010 17:39:02 +0200 wenzelm tuned;
Sun, 12 Sep 2010 16:06:03 +0200 wenzelm tuned messages;
Tue, 01 Jun 2010 11:30:57 +0200 berghofe merged
Tue, 01 Jun 2010 11:16:16 +0200 berghofe assign now applies meet before update_new to avoid misleading error message.
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Sat, 06 Feb 2010 20:57:07 +0100 wenzelm fixed spelling;
Thu, 23 Jul 2009 16:53:00 +0200 wenzelm paramify_vars: Term_Subst.map_atypsT_same
Thu, 23 Jul 2009 09:38:22 +0200 berghofe Purely functional type inference.
Fri, 17 Jul 2009 22:51:18 +0200 wenzelm tuned;
Tue, 14 Jul 2009 12:10:01 +0200 wenzelm tuned paramify_vars: Term_Subst.map_atypsT_option;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Fri, 27 Feb 2009 16:38:52 +0100 wenzelm eliminated NJ's List.nth;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 18 Jun 2008 22:32:02 +0200 wenzelm improved error output -- variant/mark bounds;
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Sat, 29 Sep 2007 21:39:49 +0200 wenzelm added fixate_params;
Sun, 23 Sep 2007 22:23:33 +0200 wenzelm constrain: canonical argument order;
Fri, 31 Aug 2007 23:17:22 +0200 wenzelm exported is_param;
Thu, 30 Aug 2007 15:04:44 +0200 wenzelm infer_types: general check_typs instead of Type.cert_typ_mode;
Tue, 14 Aug 2007 23:23:00 +0200 wenzelm infer_types: depend on Type.mode;
Mon, 23 Apr 2007 20:44:10 +0200 wenzelm added paramify_vars;
Sun, 15 Apr 2007 14:31:57 +0200 wenzelm moved get_sort to sign.ML;
Sat, 14 Apr 2007 17:38:30 +0200 wenzelm tuned comment;
Sat, 14 Apr 2007 17:36:05 +0200 wenzelm Term.string_of_vname;
Wed, 04 Oct 2006 14:17:38 +0200 haftmann insert replacing ins ins_int ins_string
Wed, 27 Sep 2006 21:13:11 +0200 wenzelm internal params: Vartab instead of AList;
Thu, 21 Sep 2006 19:04:49 +0200 wenzelm tuned;
Wed, 19 Jul 2006 12:12:04 +0200 wenzelm Name.context for used'';
Tue, 11 Jul 2006 12:17:01 +0200 wenzelm Name.invent_list;
Fri, 05 May 2006 21:59:45 +0200 wenzelm added syntax for _type_constraint_;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Tue, 25 Apr 2006 22:23:30 +0200 wenzelm refer to structure Type instead of Sorts;
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct;
Sat, 11 Feb 2006 17:17:47 +0100 wenzelm tuned;
Fri, 10 Feb 2006 02:22:37 +0100 wenzelm decode: observe Syntax.constN;
Tue, 07 Feb 2006 19:56:45 +0100 wenzelm renamed gen_duplicates to duplicates;
Mon, 06 Feb 2006 20:59:06 +0100 wenzelm tuned;
Fri, 02 Dec 2005 22:54:48 +0100 wenzelm added mixfixT;
Tue, 20 Sep 2005 08:21:49 +0200 haftmann slight adaptions to library changes
less more (0) -60 tip