diff options
| author | Pierre-Marie Pédrot | 2018-10-31 01:01:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-31 01:01:21 +0100 |
| commit | 20752cb329262ddb4b4a9ba898fd8566bf5ad156 (patch) | |
| tree | a0c04fd5ad497f97697ea182d38bd76234721270 /test-suite | |
| parent | d32301dde8071acc914286c675b9749e27f368d2 (diff) | |
| parent | 57a0d5091a9524d35161875a884835a573d82e0b (diff) | |
Merge PR #8849: Fix for bug #8848.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_8848.v | 18 |
1 files changed, 18 insertions, 0 deletions
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. |