From becc50a8ac662d666cbe2645d7d84a7ee7b0b8e4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 May 2013 22:47:22 +0000
Subject: Reporting the change on matching partial applications in patterns of
 the form "_ pat1 ... patn", and considering it experimental at this stage.

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

diff --git a/CHANGES b/CHANGES
index 6b6892e1d5..71bc1cc720 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,6 +39,10 @@ Tactics
   (potential source of rare incompatibilities).
 - Tactic "intro H" now reduces beta-iota redexes if these hide a product
   (potential source of rare incompatibilities).
+- In Ltac matching on patterns of the form "_ pat1 ... patn" now
+  behaves like if matching on "?X pat1 ... patn", i.e. accepting "_"
+  to be instantiated by an applicative term (experimental at this
+  stage, potential source of incompatibilities).
 
 Program
 
-- 
cgit v1.2.3