From 19394cc1e21c775e2151eea07970a98e6ddbce6a Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 31 Jul 2014 14:26:18 +0200
Subject: CHANGES: [numgoals] and [guard].

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

diff --git a/CHANGES b/CHANGES
index 50edd1795c..2d5216d6b7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -96,6 +96,9 @@ Tactics
     simple fix is to rewrite the recursive calls as follows: let rec t
     := constructor;[t..] which recovers the earlier behaviour. (source
     of rare incompatibilities)
+  * New tactic language feature "numgoals" to count number of goals.
+    Accompanied by "guard" tactic which fails if a boolean test does
+    not pass.
   * The refine tactic is changed not to use an ad hoc typing algorithm
     to generate subgoals. It also uses the dependent subgoal feature
     to generate goals to materialise every existential variable which
-- 
cgit v1.2.3