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/tactics.ml | |
| parent | 5c7d5fce3ed1de62ff5e1528a12adce0cdf2b0d9 (diff) | |
Replacing tclENV with the goal environment
In functions match_eqdec and check_unused_names
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 15 |
1 files changed, 9 insertions, 6 deletions
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 [] |