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.
---
 pretyping/indrec.ml           | 2 +-
 test-suite/bugs/closed/4670.v | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4670.v

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0588dcc87f..589b8d82ab 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -598,7 +598,7 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = repr_mind kn in
+  let mp,dp,l = KerName.repr (MutInd.canonical kn) in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
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