diff options
author | amblaf <you@example.com> | 2017-06-20 09:48:55 +0200 |
---|---|---|
committer | amblaf <you@example.com> | 2017-07-31 10:34:05 +0200 |
commit | b84ab413f8434719dbbf5e09da9a0698b84b0106 (patch) | |
tree | 5cbbc30806d595126f381518a8a0d83bc16394b4 /tactics | |
parent | 5c7d5fce3ed1de62ff5e1528a12adce0cdf2b0d9 (diff) |
Replacing tclENV with the goal environment
In functions match_eqdec and check_unused_names
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/eqdecide.ml | 9 | ||||
-rw-r--r-- | tactics/tactics.ml | 15 |
2 files changed, 14 insertions, 10 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 282b020ba..e16fcec7c 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -155,8 +155,7 @@ open Proofview.Notations (* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) -let match_eqdec sigma c = - Proofview.tclENV >>= fun env -> +let match_eqdec env sigma c = try let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in let (op,eq1,noteq,eq2) = @@ -203,8 +202,9 @@ let solveEqBranch rectype = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in @@ -230,8 +230,9 @@ let decideGralEquality = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> let headtyp = hd_app sigma (pf_compute gl typ) in begin match EConstr.kind sigma headtyp with | Ind (mi,_) -> Proofview.tclUNIT mi diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5920b344d..b194ac5a9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3074,17 +3074,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] *) -let warn_unused_intro_pattern env = +let warn_unused_intro_pattern env sigma = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" (fun names -> strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c env Evd.empty)))) names) + (fun c -> Printer.pr_econstr (snd (c env sigma)))) names) -let check_unused_names names env = +let check_unused_names env sigma names = if not (List.is_empty names) then - warn_unused_intro_pattern env names + warn_unused_intro_pattern env sigma names let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous @@ -3204,9 +3204,12 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = peel_tac ra' dests names thin) end | [] -> - Proofview.tclENV >>= fun env -> - check_unused_names names env; + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + check_unused_names env sigma names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) + end in peel_tac ra dests names [] |