Removing tclEVARS in various places.

7 files changed, 54 insertions, 37 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 617c491c3..9ca6162a2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -117,10 +117,11 @@ let exact poly (c,clenv) =
       let ctx = Evd.evar_universe_context clenv.evd in
 	ctx, c
   in
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
-    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c')
-  end
+  Proofview.Goal.s_enter { enter = begin fun gl sigma ->
+    let sigma = Sigma.to_evar_map sigma in
+    let sigma = Evd.merge_universe_context sigma ctx in
+    Sigma.Unsafe.of_pair (exact_check c', sigma)
+  end }
 
 (* Util *)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3a9d40de0..9892d2954 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -18,6 +18,8 @@ open Util
 open Tacexpr
 open Mod_subst
 open Locus
+open Sigma.Notations
+open Proofview.Notations
 
 (* Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
@@ -91,14 +93,15 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tac
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = find_rewrites bas in
-  let try_rewrite dir ctx c tc = Proofview.Goal.nf_enter (fun gl ->
+  let try_rewrite dir ctx c tc =
+  Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
     let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Sigma.to_evar_map sigma in
     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
-    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-      (general_rewrite_maybe_in dir c' tc)
-  ) in
+    let tac = general_rewrite_maybe_in dir c' tc in
+    Sigma.Unsafe.of_pair (tac, sigma)
+  end } in
   let lrul = List.map (fun h -> 
   let tac = match h.rew_tac with None -> Proofview.tclUNIT () | Some t -> Tacinterp.eval_tactic t in
     (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 22f218b4f..025374764 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -13,6 +13,8 @@ open Tactics
 open Coqlib
 open Reductionops
 open Misctypes
+open Sigma.Notations
+open Proofview.Notations
 
 (* Absurd *)
 
@@ -22,18 +24,19 @@ let mk_absurd_proof t =
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.s_enter { enter = begin fun gl sigma ->
     let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Sigma.to_evar_map sigma in
     let j = Retyping.get_judgment_of env sigma c in
     let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
     let t = j.Environ.utj_val in
+    let tac =
     Tacticals.New.tclTHENLIST [
-      Proofview.Unsafe.tclEVARS sigma;
       elim_type (build_coq_False ());
       Simple.apply (mk_absurd_proof t)
-    ]
-  end
+    ] in
+    Sigma.Unsafe.of_pair (tac, sigma)
+  end }
 
 let absurd c = absurd c
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a74d555dd..1f6669900 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 ->
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 3d544274d..43a31b04f 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -15,6 +15,7 @@ open Refiner
 open Evd
 open Locus
 open Sigma.Notations
+open Proofview.Notations
 
 (* The instantiate tactic *)
 
@@ -69,17 +70,17 @@ let instantiate_tac_by_name id c =
 
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+  Proofview.Goal.s_enter { enter = begin fun gl sigma ->
     let env = Proofview.Goal.env gl in
     let id = match name with
     | Names.Anonymous -> 
       let id = Namegen.id_of_name_using_hdchar env typ name in
       Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
-    | Names.Name id -> id in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (evar, sigma', _) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
-      let sigma' = Sigma.to_evar_map sigma' in
-    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
+    | Names.Name id -> id
+    in
+    let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+    let tac =
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
-  end
+    in
+    Sigma (tac, sigma, p)
+  end }
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index d7d82111c..f543a7691 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -617,8 +617,8 @@ let out_arg = function
   | ArgArg x -> x
 
 let hResolve id c occ t =
-  Proofview.Goal.nf_enter begin fun gl ->
-  let sigma = Proofview.Goal.sigma gl in
+  Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
+  let sigma = Sigma.to_evar_map sigma in
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
   let env_ids = Termops.ids_of_context env in
@@ -636,10 +636,11 @@ let hResolve id c occ t =
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
-  Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARS sigma)
+  let tac =
     (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))
-  end
+  in
+  Sigma.Unsafe.of_pair (tac, sigma)
+  end }
 
 let hResolve_auto id c t =
   let rec resolve_auto n = 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0acaeb44c..85f2d2f91 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -432,8 +432,8 @@ let rewrite_equations_tac as_mode othin id neqns names ba =
     tac
 
 let raw_inversion inv_kind id status names =
-  Proofview.Goal.nf_enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+  Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
+    let sigma = Sigma.to_evar_map sigma in
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
@@ -462,7 +462,7 @@ let raw_inversion inv_kind id status names =
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
-    tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    let tac =
       (tclTHENS
         (assert_before Anonymous cut_concl)
         [case_tac names
@@ -470,7 +470,9 @@ let raw_inversion inv_kind id status names =
                (rewrite_equations_tac as_mode inv_kind id neqns))
             (Some elim_predicate) ind (c, t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
-  end
+    in
+    Sigma.Unsafe.of_pair (tac, sigma)
+  end }
 
 (* Error messages of the inversion tactics *)
 let wrap_inv_error id = function (e, info) -> match e with