From a36f148dd86a258cd15f5a24678caa3ad7bb76ca Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 9 Jun 2008 15:11:59 +0000
Subject: Documentation de "instantiate".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11080 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 5cf6e5ae6e..c2e6c741f3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -247,6 +247,7 @@ Tactics
   matching lemma among the components of the conjunction; tactic apply also
   able to apply lemmas of conclusion an empty type.
 - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
+- New tactic "instantiate" (without argument).
 - Tactic firstorder "with" and "using" options have their meaning swapped for
   consistency with auto/eauto (source of incompatibility).
 - Tactic "generalize" now supports "at" options to specify occurrences
-- 
cgit v1.2.3