From 57a0d5091a9524d35161875a884835a573d82e0b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 Oct 2018 22:04:16 +0100
Subject: Fix for bug #8848

---
 test-suite/bugs/closed/bug_8848.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8848.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_8848.v b/test-suite/bugs/closed/bug_8848.v
new file mode 100644
index 0000000000..26563e6747
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8848.v
@@ -0,0 +1,18 @@
+Require Import Program.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Definition def (a : nat) := a = a.
+
+Structure record {a : nat} {D : def a} :=
+  inR { prop : Prop }.
+
+Program
+Canonical Structure ins (a : nat) (rec : @record a _) :=
+  @inR a _ (prop rec).
+Next Obligation.
+  exact eq_refl.
+Defined.
+Next Obligation.
+  exact eq_refl.
+Defined.
-- 
cgit v1.2.3