CHANGES: untyped terms in tactics

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 9b517d9b3d..ebef67e89c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -165,6 +165,7 @@ Tactics
   has been cleared or renamed in the current goal context now fail
   (possible source of incompatibilities solvable by avoiding clearing
   the relevant hypotheses).
+- New construct "uconstr:c" and "type_term c" to build untyped terms.
 
 
 Program