From b18a6d179903546cbf5745e601ab221f06e30078 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 29 Dec 2008 17:15:52 +0000
Subject: - Added support for subterm matching in SearchAbout. - Backtrack on
 precise unfolding of "iff" in "tauto": it has effects on   the naming of
 hypotheses (especially when doing "case H" with H of   type "{x|P<->Q}" since
 not unfolding will eventually introduce a name   "i" while unfolding will
 eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a
 plugin is missing, doc hnf, standardization   of names manipulating type
 constr_pattern, ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/changes.txt | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 9488f1dead..cae948a003 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -18,6 +18,9 @@ Eauto.simplest_apply -> Hiddentac.h_simplest_apply
 Evarutil.define_evar_as_arrow -> define_evar_as_product
 Old version of Tactics.assert_tac disappears
 Tactics.true_cut renamed into Tactics.assert_tac
+Constrintern.interp_constrpattern -> intern_constr_pattern
+Hipattern.match_with_conjunction is a bit more restrictive
+Hipattern.match_with_disjunction is a bit more restrictive
 
 ** Universe names (univ.mli)
 
-- 
cgit v1.2.3