diff options
| -rw-r--r-- | pretyping/indrec.ml | 8 |
1 files 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 -> |