From 4b429f64ee9a36a7151575b914b3af56a300b28b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Dec 2019 20:28:42 +0100
Subject: 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.
---
 test-suite/bugs/closed/bug_11114.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11114.v

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3