@@ -7,6 +7,9 @@ Language updates
7* Improved unification by implementing a pattern unification rule
7* Improved unification by implementing a pattern unification rule
8* The syntax `{{n}} quotes n without resolving it, allowing short syntax
8* The syntax `{{n}} quotes n without resolving it, allowing short syntax
9 for defining new names. `{n} still quotes n to an existing name in scope.
9 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.
11Library updates
14Library updates
12---------------
15---------------