Not taking arguments given by name or position into account when

computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.

For instance, "eq_refl (A:=nat)" is  now interpreted as "@eq_refl nat _",
the same way as if we had said:

Arguments eq_refl {A} {x}.

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index fa0e70ba0a..db27f82001 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes beyond V8.5
 ===================
 
+Specification language
+
+- Giving implicit arguments explicitly to a constant with multiple
+  choices of implicit arguments does not break any more insertion of
+  further maximal implicit arguments.
+
 Tactics
 
 - Flag "Bracketing Last Introduction Pattern" is now on by default.