aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorInCanonicalStructures2.v
diff options
context:
space:
mode:
authorPaul Steckler2018-02-06 15:13:17 -0500
committerPaul Steckler2018-02-06 15:13:17 -0500
commit3e36e6100f78e564642992801fae6fe75fd13d3d (patch)
treef5a5093b3a3b60079071014292446b510998818b /test-suite/output/ErrorInCanonicalStructures2.v
parentb1d56e48b2453814a5d2898688fbc7c5d29d32fa (diff)
More detailed error messages for Canonical Structure, #6398
Diffstat (limited to 'test-suite/output/ErrorInCanonicalStructures2.v')
-rw-r--r--test-suite/output/ErrorInCanonicalStructures2.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v
new file mode 100644
index 0000000000..10ee177aaf
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.v
@@ -0,0 +1,3 @@
+Definition bar := 99.
+
+Canonical Structure bar.