changeset 16104 | dab13c4685ba |
parent 16102 | c5f6726d9bb1 |
child 16111 | d06dc7975731 |
--- a/NEWS Fri May 27 16:33:33 2005 +0200 +++ b/NEWS Fri May 27 17:10:23 2005 +0200 @@ -78,7 +78,7 @@ * Pure: print_tac now outputs the goal through the trace channel. -* Pure: reference Namespace.unique_names included. If true the +* Pure: reference NameSpace.unique_names included. If true the (shortest) namespace-prefix is printed to disambiguate conflicts (as yet). If false the first entry wins (as during parsing). Default value is true.