Replacing tclENV with the goal environment

In functions match_eqdec and check_unused_names

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 []