From a31b978d3477d5977d87781190df136462aeea1d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 29 Jul 2014 17:58:53 +0200
Subject: CHANGES: untyped terms in tactics

---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

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
-- 
cgit v1.2.3