From 741f3fab052b91eaec57f32b639ca722c3d8dc34 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Mar 2017 13:18:42 +0100
Subject: A fix for #5390 (a useful error on used introduction names was
 masked).

With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.

We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.

Of course, the question of what best unification error to give in the
presence of backtracking is still open.
---
 COMPATIBILITY | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index d423e71df3..78dfabaa3e 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,10 @@
+Potential sources of incompatibilities between Coq V8.6 and V8.7
+----------------------------------------------------------------
+
+- Extra superfluous names in introduction patterns may now raise an
+  error rather than a warning when the superfluous name is already in
+  use. The easy fix is to remove the superfluous name.
+
 Potential sources of incompatibilities between Coq V8.5 and V8.6
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3