diff options
| author | Maxime Dénès | 2019-04-04 18:17:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | 3b980d937b5adfbae472ed8a13748a451fdf3450 (patch) | |
| tree | a3a2fcc4273df543218dbde93a5a5a4934fb0fea /pretyping | |
| parent | 8fe32139aeb965b056c0d1e9c8fab2324dbb7ba6 (diff) | |
Remove calls to global env from indrec
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 |