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.
---
 test-suite/bugs/closed/bug_9508.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9508.v

(limited to 'test-suite/bugs')

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