Update CHANGELOG for deprecated tactics
commitf4bcbbcd2f9de4af6023439e554b5f80e151d3ba
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateThu 10 Sep 2015, 08:26 (11 years ago)
parentdfb42d1
CHANGELOG+3
@@ -7,6 +7,9 @@ Language updates
77* Improved unification by implementing a pattern unification rule
88* The syntax `{{n}} quotes n without resolving it, allowing short syntax
99 for defining new names. `{n} still quotes n to an existing name in scope.
10+* The previous syntax for tactic proofs and the previous interactive prover
11+ are now deprecated in favour of reflected elaboration. They will be removed
12+ at some point in the future.
1013
1114Library updates
1215---------------