| Mon, 08 Sep 2014 16:09:10 +0200 |
blanchet |
made code work also in the presence of deads
|
changeset |
files
|
| Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
changeset |
files
|
| Mon, 08 Sep 2014 15:12:35 +0200 |
blanchet |
test sorts
|
changeset |
files
|
| Mon, 08 Sep 2014 15:11:37 +0200 |
blanchet |
use right sort constraints
|
changeset |
files
|
| Mon, 08 Sep 2014 14:04:03 +0200 |
blanchet |
never include hidden names -- these cannot be referenced afterward
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:46 +0200 |
blanchet |
made SML/NJ happire
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:40 +0200 |
blanchet |
export useful functions for users of (co)recursors
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:35 +0200 |
blanchet |
improved caching
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:13 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:08 +0200 |
blanchet |
wildcards in plugins
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
improved 'datatype_compat' further for recursion through functions
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
no type-based lookup -- these fail in the general, ambiguous case
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
more examples/tests
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuned docs
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
properly note theorems for split recursors
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
export one more ML function
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
more compatibility documentation
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:28 +0200 |
blanchet |
refactored MaSh files to avoid regenerating exports on each eval
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
added missing 'transpose'
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
|
changeset |
files
|
| Mon, 08 Sep 2014 09:52:06 +0200 |
traytel |
made tactic more robust w.r.t. dead variables
|
changeset |
files
|