aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES1
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