Fixing #11114 (anomaly with Extraction Implicit on records).

This was due to an inconsistency in handling implicit arguments in
the fields and in the constructor of a record.

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_11114.v b/test-suite/bugs/closed/bug_11114.v
new file mode 100644
index 0000000000..dd981279db
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11114.v
@@ -0,0 +1,17 @@
+Require Extraction.
+
+Inductive t (sig: list nat) :=
+| T (k: nat).
+
+Record pkg :=
+  { _sig: list nat;
+    _t : t _sig }.
+
+Definition map (f: nat -> nat) (p: pkg) :=
+  {| _sig := p.(_sig);
+     _t := match p.(_t) with
+          | T _ k => T p.(_sig) (f k)
+          end |}.
+
+Extraction Implicit Build_pkg [_sig].
+Extraction TestCompile map.