From 23058c691868165b0aa5e32beb92a7bb07bc4b12 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 8 Sep 2014 10:55:10 +0200
Subject: CHANGES: Ltac's [refine] accepts [uconstr].

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES b/CHANGES
index 80ac8987b4..c8ad42d2fe 100644
--- a/CHANGES
+++ b/CHANGES
@@ -177,6 +177,8 @@ Tactics
 - New construct "uconstr:c" and "type_term c" to build untyped terms.
 - Binders in terms defined in Ltac (either "constr" or "uconstr") can
   now take their names from identifier defined in Ltac.
+- The "refine" tactic now accepts untyped terms built with "uconstr"
+  so that terms with holes can be constructed piecewise in Ltac.
 - New bullets --, ++, **, ---, +++, ***, ... made available.
 - The good bullet is suggested sometimes when user gives a wrong one.
 - New tactic "enough", symmetric to "assert", but with subgoals
-- 
cgit v1.2.3