Removing tclEVARS in various places.

1 files changed, 12 insertions, 6 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index a74d555dd0..1f66699004 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,6 +40,7 @@ open Eqschemes
 open Locus
 open Locusops
 open Misctypes
+open Sigma.Notations
 open Proofview.Notations
 open Unification
 
@@ -346,17 +347,20 @@ let type_of_clause cls gl = match cls with
   | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun c type_of_cls in
   let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*>
+  let tac =
+      Proofview.tclEFFECTS effs <*>
       general_elim_clause with_evars frzevars tac cls c t l
       (match lft2rgt with None -> false | Some b -> b)
       {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
-  end
+  in
+  Sigma.Unsafe.of_pair (tac, sigma)
+  end }
 
 let adjust_rewriting_direction args lft2rgt =
   match args with
@@ -1472,19 +1476,21 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in
+  let tac =
   tclTHENFIRST
     (tclTHENLIST [
-       (Proofview.Unsafe.tclEVARS sigma);
        (change_concl typ); (* Put in pattern form *)
        (replace_core onConcl l2r eqn)
     ])
     (change_concl expected) (* Put in normalized form *)
-   end
+  in
+  Sigma.Unsafe.of_pair (tac, sigma)
+  end }
 
 let cutSubstInHyp l2r eqn id =
   Proofview.Goal.nf_enter begin fun gl ->