| Tue, 19 Apr 2011 10:37:38 +0200 |
wenzelm |
more precise treatment of existing type inference parameters;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 12:11:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 22:54:54 +0200 |
wenzelm |
more sharing of operations, without aliases;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 13:20:18 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 12:42:08 +0200 |
wenzelm |
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:35:55 +0200 |
wenzelm |
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 22:28:59 +0200 |
wenzelm |
Type_Infer.preterm: eliminated separate Constraint;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 21:24:23 +0200 |
wenzelm |
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 20:47:47 +0200 |
wenzelm |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:55:45 +0200 |
wenzelm |
common Type.appl_error, which also covers explicit constraints;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 17:39:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 16:06:03 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:30:57 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:16:16 +0200 |
berghofe |
assign now applies meet before update_new to avoid misleading error message.
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 20:57:07 +0100 |
wenzelm |
fixed spelling;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 16:53:00 +0200 |
wenzelm |
paramify_vars: Term_Subst.map_atypsT_same
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 09:38:22 +0200 |
berghofe |
Purely functional type inference.
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 22:51:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 12:10:01 +0200 |
wenzelm |
tuned paramify_vars: Term_Subst.map_atypsT_option;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 16:38:52 +0100 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 22:32:02 +0200 |
wenzelm |
improved error output -- variant/mark bounds;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|