Documenting the tactic-in-term construction.

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index f74566ec63..6b8663b678 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,7 @@ Specification Language
   now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
   (possible source of incompatibilities)
 - Slight changes in unification error messages.
+- Added a syntax $(...)$ allowing to put tactics in terms.
 
 Tactics