diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/indrec.ml | 6 | ||||
| -rw-r--r-- | pretyping/indrec.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 29fc62af02..7615a17514 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -610,11 +610,11 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s) (* Look up function for the default elimination constant *) -let lookup_eliminator ind_sp s = +let lookup_eliminator env ind_sp s = let kn,i = ind_sp 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 ind_id = (lookup_mind kn env).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 @@ -623,7 +623,7 @@ let lookup_eliminator ind_sp s = (* inductive type *) try let cst = Constant.make knu knc in - let _ = Global.lookup_constant cst in + let _ = lookup_constant cst env in ConstRef cst with Not_found -> (* Then try to get a user-defined eliminator in some other places *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 91a5651f7f..8eb571a8be 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -62,7 +62,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> (** Recursor names utilities *) -val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t +val lookup_eliminator : env -> inductive -> Sorts.family -> GlobRef.t val elimination_suffix : Sorts.family -> string val make_elimination_ident : Id.t -> Sorts.family -> Id.t |