| changeset 59112 | e670969f34df |
| parent 59105 | 18d4e100c267 |
| child 59139 | e557a9ddee5f |
--- a/NEWS Mon Dec 08 16:04:50 2014 +0100 +++ b/NEWS Mon Dec 08 22:42:12 2014 +0100 @@ -218,6 +218,9 @@ *** ML *** +* Cartouches within ML sources are turned into values of type +Input.source (with formal position information). + * Proper context for various elementary tactics: assume_tac, match_tac, compose_tac, Splitter.split_tac etc. Minor INCOMPATIBILITY.