From 8fe32139aeb965b056c0d1e9c8fab2324dbb7ba6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 17:09:07 +0200
Subject: Fix constant order in heads.ml

As per the OCaml documentation, the order for maps should be total.
I also remove some circumvolutions that were added around eliminators
and canonical names because of this incorrect order.
---
 pretyping/indrec.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 4f940fa16a..29fc62af02 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -612,13 +612,17 @@ 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,l = KerName.repr (MutInd.canonical kn) in
+  let mpu = KerName.modpath @@ MutInd.user kn in
+  let mpc = KerName.modpath @@ 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
+  let l = Label.of_id id in
+  let knu = KerName.make mpu l in
+  let knc = KerName.make mpc l in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta_kn (KerName.make mp (Label.of_id id)) in
+    let cst = Constant.make knu knc in
     let _ = Global.lookup_constant cst in
       ConstRef cst
   with Not_found ->
-- 
cgit v1.2.3