aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-30 16:44:56 +0200
committerMaxime Dénès2018-05-30 16:44:56 +0200
commit3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (patch)
treecbdc56e553e3d6f4a9d56a679f000f43570ed1a5 /test-suite
parentb75f714c025b51ed8b4db15bfce99df2d6ae7c41 (diff)
parent0ab081179fc448286c4cb0e9fcd4f67c37ed964c (diff)
Merge PR #7260: Fix #6951: Unexpected error during scheme creation.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/6951.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/6951.v b/test-suite/bugs/closed/6951.v
new file mode 100644
index 0000000000..419f8d7c4e
--- /dev/null
+++ b/test-suite/bugs/closed/6951.v
@@ -0,0 +1,2 @@
+Record float2 : Set := Float2 { Fnum : unit }.
+Scheme Equality for float2.