author | ballarin |
Fri, 27 May 2005 17:10:23 +0200 | |
changeset 16104 | dab13c4685ba |
parent 16103 | 323838df22fd |
child 16105 | a44801c499cb |
--- 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.