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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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 *)
-- 
cgit v1.2.3