From a0116bdcb169ebe6e891a7bb3b9e642b9082a0a7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Feb 2019 16:24:32 +0100
Subject: Fix #9508: Unexpected interaction between implicit arguments and
 primitive projections.

This was due to an involuntary capture of a variable name.
---
 CHANGES.md                        |  3 +++
 interp/impargs.ml                 |  2 +-
 test-suite/bugs/closed/bug_9508.v | 29 +++++++++++++++++++++++++++++
 3 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_9508.v

diff --git a/CHANGES.md b/CHANGES.md
index 26573b9185..08519eb1fb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -130,6 +130,9 @@ Vernacular commands
   for all commands that support it. In particular, it does not have any effect
   on tactics anymore. May cause some incompatibilities.
 
+- The algorithm computing implicit arguments now behaves uniformly for primitive
+  projection and application nodes (bug #9508).
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 959455dfd2..7e8f2f4f3d 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -200,7 +200,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
 	if strict then () else
           iter_with_full_binders sigma push_lift (frec false) ed c
-    | Proj (p,c) when rig ->
+    | Proj (p, _) when rig ->
       if strict then () else
         iter_with_full_binders sigma push_lift (frec false) ed c
     | Case _ when rig ->
diff --git a/test-suite/bugs/closed/bug_9508.v b/test-suite/bugs/closed/bug_9508.v
new file mode 100644
index 0000000000..2c38e24add
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9508.v
@@ -0,0 +1,29 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Module OK.
+Record A := mkA {
+  T : Type;
+  P : T -> bool;
+}.
+
+About P. (* Argument a is implicit *)
+Check P (true: T (mkA negb)).
+End OK.
+
+Module KO.
+Set Primitive Projections.
+Record A := mkA {
+  T : Type;
+  P : T -> bool;
+}.
+
+About P. (* No implicit arguments *)
+Check P (true: T (mkA negb)).
+(*
+The command has indeed failed with message:
+The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}"
+while it is expected to have type "A".
+*)
+
+End KO.
-- 
cgit v1.2.3