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 /tactics | |
| parent | 8fe32139aeb965b056c0d1e9c8fab2324dbb7ba6 (diff) | |
Remove calls to global env from indrec
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
3 files changed, 6 insertions, 4 deletions
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 |