| Revision 16147,
925 bytes
checked in by broeni, 4 years ago
(diff) |
|
think I fixed replace and added a bound_spass function to alpha that has the functionality of the old free_spass function, but just the bound part
|
| Line | |
|---|
| 1 | - proc-dec - precatch zeroary destructors |
|---|
| 2 | |
|---|
| 3 | - everywhere where a new binding is added, use alpha renaming to check that a new name is introduced and alpha rename in the rest of the process |
|---|
| 4 | |
|---|
| 5 | Kind-Pair, Sub-Pair-Cov, Alg-Pair, Alg-Second, Alg-Proc-In, Proc-New, Alg-Proc-Des, Alg-Proc-Second, Proc-Par |
|---|
| 6 | |
|---|
| 7 | - positive/binders-03.spi - parser bug Spass bug |
|---|
| 8 | |
|---|
| 9 | - negative/kinding-bad-02.spi - not parseable |
|---|
| 10 | |
|---|
| 11 | - bugs/x.spi now succeeds.. ? |
|---|
| 12 | |
|---|
| 13 | |
|---|
| 14 | pseudo-trust is not a bug with the comment, it is a bug when parsing formulas, here exists x. is not SPASS syntax. exists(x, ..., blah) |
|---|
| 15 | |
|---|
| 16 | - STM ?!?!?!?!? |
|---|
| 17 | |
|---|
| 18 | - now 0 is a number too so we cannot use it any longer as Stop |
|---|
| 19 | |
|---|
| 20 | - functions.ml: two open questions in functions |
|---|
| 21 | - environment.ml: formulas: fiddle the formulas out of refinement types? |
|---|
| 22 | - environment.ml: well_formed': EBind seems wrong |
|---|
| 23 | - replace.ml: rename_process: pattern matching not exhaustive |
|---|
| 24 | - replace.ml: replace_stmt_in_type': Refine |
|---|
Note: See
TracBrowser
for help on using the repository browser.
