diff options
| -rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 6 | ||||
| -rw-r--r-- | pretyping/indrec.mli | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
8 files changed, 14 insertions, 12 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a5c19f3217..e582362e25 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let _ = List.map_i (fun i x -> - let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in - let env = Global.env () in + let env = Global.env () in + let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 350bb9019e..675e4d2457 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let sort = Tacticals.elimination_sort_of_goal gl in let gl, elim = if not is_case then - let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in + let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in gl, t else Tacmach.pf_eapply (fun env sigma () -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 5abbc214de..a7a3fee942 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in - let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in + let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in 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 diff --git a/tactics/equality.ml b/tactics/equality.ml index 412fbbfd1b..d5fdad0127 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot = match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> let pr1 = - lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) + lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) in begin match lft2rgt, cls with | Some true, None diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ec8d4d0e14..dcd63fe760 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -704,7 +704,8 @@ module New = struct (* computing the case/elim combinators *) let gl_make_elim ind = begin fun gl -> - let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in + let env = Proofview.Goal.env gl in + let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in let (sigma, c) = pf_apply Evd.fresh_global gl gr in (sigma, c) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 206f35c8ba..53a74a5f7d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1455,7 +1455,8 @@ exception IsNonrec let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite let find_ind_eliminator ind s gl = - let gr = lookup_eliminator ind s in + let env = Proofview.Goal.env gl in + let gr = lookup_eliminator env ind s in Tacmach.New.pf_apply Evd.fresh_global gl gr let find_eliminator c gl = @@ -4128,7 +4129,7 @@ let guess_elim isrec dep s hyp0 gl = let sigma, elimc = if isrec && not (is_nonrec mind) then - let gr = lookup_eliminator mind s in + let gr = lookup_eliminator env mind s in Evd.fresh_global env sigma gr else let u = EInstance.kind sigma u in |