equal
deleted
inserted
replaced
76 translations) resulting from the given syntax specification, which |
76 translations) resulting from the given syntax specification, which |
77 is interpreted in the same manner as for the 'syntax' command. |
77 is interpreted in the same manner as for the 'syntax' command. |
78 |
78 |
79 * Pure: print_tac now outputs the goal through the trace channel. |
79 * Pure: print_tac now outputs the goal through the trace channel. |
80 |
80 |
81 * Pure: reference Namespace.unique_names included. If true the |
81 * Pure: reference NameSpace.unique_names included. If true the |
82 (shortest) namespace-prefix is printed to disambiguate conflicts (as |
82 (shortest) namespace-prefix is printed to disambiguate conflicts (as |
83 yet). If false the first entry wins (as during parsing). Default |
83 yet). If false the first entry wins (as during parsing). Default |
84 value is true. |
84 value is true. |
85 |
85 |
86 * Pure: tuned internal renaming of symbolic identifiers -- attach |
86 * Pure: tuned internal renaming of symbolic identifiers -- attach |