From 443857fe1bbecf089eb40d522a71a014273c5a23 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 14:06:17 +0200
Subject: Use the canonical name when looking for an eliminator (bug #4670).

Disclaimer: I have no idea what I am doing.
---
 test-suite/bugs/closed/4670.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4670.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v
new file mode 100644
index 0000000000..6113992953
--- /dev/null
+++ b/test-suite/bugs/closed/4670.v
@@ -0,0 +1,7 @@
+Require Import Coq.Vectors.Vector.
+Module Bar.
+  Definition foo A n (l : Vector.t A n) : True.
+  Proof.
+    induction l ; exact I.
+  Defined.
+End Bar.
-- 
cgit v1.2.3