Proofview: split [V82] module into [Unsafe] and [V82].

The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.

11 files changed, 67 insertions, 67 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 39b1ff3c0..18beedf95 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -103,7 +103,7 @@ let exact poly (c,clenv) =
   in
   Proofview.Goal.enter begin fun gl ->
     let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
-    Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) (exact_check c')
+    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c')
   end
 
 (* Util *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index a51c4a962..2be8020a7 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -96,7 +96,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
     let c' = Vars.subst_univs_level_constr subst c in
     let sigma = Proofview.Goal.sigma gl in
     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
-    Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma)
+    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (general_rewrite_maybe_in dir c' tc)
   ) in
   let lrul = List.map (fun h -> 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index cb1b7d557..9a241c7ef 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -31,7 +31,7 @@ let absurd c =
     let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
     let t = j.Environ.utj_val in
     Tacticals.New.tclTHENLIST [
-      Proofview.V82.tclEVARS sigma;
+      Proofview.Unsafe.tclEVARS sigma;
       elim_type (build_coq_False ());
       Simple.apply (mk_absurd_proof t)
     ]
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index a464b5e8d..93768c10a 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -71,7 +71,7 @@ END
 TACTIC EXTEND left_with
   [ "left" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.V82.tclEVARS sigma <*> Tactics.left_with_bindings false bl
+    Proofview.Unsafe.tclEVARS sigma <*> Tactics.left_with_bindings false bl
   ]
 END
 
@@ -95,7 +95,7 @@ END
 TACTIC EXTEND right_with
   [ "right" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.V82.tclEVARS sigma <*> Tactics.right_with_bindings false bl
+    Proofview.Unsafe.tclEVARS sigma <*> Tactics.right_with_bindings false bl
   ]
 END
 
@@ -118,7 +118,7 @@ TACTIC EXTEND constructor
     let { Evd.sigma = sigma; it = bl } = bl in
     let i = Tacinterp.interp_int_or_var ist i in
     let tac c = Tactics.constructor_tac false None i c in
-    Proofview.V82.tclEVARS sigma <*> tac bl
+    Proofview.Unsafe.tclEVARS sigma <*> tac bl
   ]
 END
 
@@ -142,7 +142,7 @@ TACTIC EXTEND specialize
   [ "specialize" constr_with_bindings(c) ] -> [
     let { Evd.sigma = sigma; it = c } = c in
     let specialize c = Proofview.V82.tactic (Tactics.specialize c) in
-    Proofview.V82.tclEVARS sigma <*> specialize c
+    Proofview.Unsafe.tclEVARS sigma <*> specialize c
   ]
 END
 
@@ -163,7 +163,7 @@ END
 TACTIC EXTEND split_with
   [ "split" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.V82.tclEVARS sigma <*> Tactics.split_with_bindings false [bl]
+    Proofview.Unsafe.tclEVARS sigma <*> Tactics.split_with_bindings false [bl]
   ]
 END
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 79e852815..425e9f290 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -238,7 +238,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
   let try_clause c =
     side_tac
       (tclTHEN
-         (Proofview.V82.tclEVARS c.evd)
+         (Proofview.Unsafe.tclEVARS c.evd)
          (general_elim_clause with_evars frzevars cls c elim))
       tac
   in
@@ -348,7 +348,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   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.V82.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*>
+    Proofview.Unsafe.tclEVARS sigma <*> 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}
@@ -925,7 +925,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
-  Proofview.V82.tclEVARS sigma <*>
+  Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
     [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))]
@@ -954,7 +954,7 @@ let onEquality with_evars tac (c,lbindc) =
   let eqn = clenv_type eq_clause' in
   let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
-    (Proofview.V82.tclEVARS eq_clause'.evd)
+    (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
   end
 
@@ -1308,7 +1308,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   if List.is_empty injectors then
     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
   else
-    Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref)
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Proofview.tclBIND
       (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
@@ -1482,7 +1482,7 @@ let cutSubstInConcl l2r eqn =
   let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in
   tclTHENFIRST
     (tclTHENLIST [
-       (Proofview.V82.tclEVARS sigma);
+       (Proofview.Unsafe.tclEVARS sigma);
        (Proofview.V82.tactic (change_concl typ)); (* Put in pattern form *)
        (replace_core onConcl l2r eqn)
     ])
@@ -1497,7 +1497,7 @@ let cutSubstInHyp l2r eqn id =
   let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in
   tclTHENFIRST
     (tclTHENLIST [
-       (Proofview.V82.tclEVARS sigma);
+       (Proofview.Unsafe.tclEVARS sigma);
        (Proofview.V82.tactic (change_in_hyp None (fun _ s -> s,typ) (id,InHypTypeOnly)));
        (replace_core (onHyp id) l2r eqn)
     ])
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 71d766e12..bce768cd4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -34,12 +34,12 @@ TACTIC EXTEND admit
 END
 
 let replace_in_clause_maybe_by (sigma,c1) c2 cl  tac =
-  Proofview.V82.tclEVARS sigma <*>
+  Proofview.Unsafe.tclEVARS sigma <*>
     (replace_in_clause_maybe_by c1 c2 cl)
     (Option.map Tacinterp.eval_tactic tac)
 
 let replace_term dir_opt (sigma,c) cl =
-  Proofview.V82.tclEVARS sigma <*>
+  Proofview.Unsafe.tclEVARS sigma <*>
     (replace_term dir_opt c) cl
 
 TACTIC EXTEND replace
@@ -202,7 +202,7 @@ END
 
 let onSomeWithHoles tac = function
   | None -> tac None
-  | Some c -> Proofview.V82.tclEVARS c.sigma <*> tac (Some c.it)
+  | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it)
 
 TACTIC EXTEND contradiction
  [ "contradiction" constr_with_bindings_opt(c) ] ->
@@ -246,7 +246,7 @@ END
 
 let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
-  Proofview.V82.tclEVARS sigma <*>
+  Proofview.Unsafe.tclEVARS sigma <*>
     general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true
 
 TACTIC EXTEND rewrite_star
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 457068c6c..62117bff7 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names =
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
-    tclTHEN (Proofview.V82.tclEVARS sigma)
+    tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (tclTHENS
         (assert_before Anonymous cut_concl)
         [case_tac names
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index b55ee7030..ec9a9ff3e 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1478,13 +1478,13 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
 	match is_hyp, prf with
 	| Some id, Some p ->
             let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.tclNEWGOALS gls in
-            Proofview.V82.tclEVARS undef <*>
+            Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
-            Proofview.V82.tclEVARS undef <*>
+            Proofview.Unsafe.tclEVARS undef <*>
             convert_hyp_no_check (id, None, newt)
 	| None, Some p ->
-            Proofview.V82.tclEVARS undef <*>
+            Proofview.Unsafe.tclEVARS undef <*>
             Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
             let make sigma =
@@ -1494,7 +1494,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
             Proofview.Refine.refine make <*> Proofview.tclNEWGOALS gls
             end
 	| None, None ->
-            Proofview.V82.tclEVARS undef <*>
+            Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
   let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f7c3c922f..8f516802d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -598,7 +598,7 @@ let new_interp_constr ist c k =
   let open Proofview in
   Proofview.Goal.enter begin fun gl ->
     let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in
-    Proofview.tclTHEN (Proofview.V82.tclEVARS sigma) (k c)
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c)
   end
 
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
@@ -1135,7 +1135,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
           let concl = Proofview.Goal.concl gl in
           let goal = Proofview.Goal.goal gl in
           let (sigma, arg) = interp_genarg ist env sigma concl goal x in
-          Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return arg)
+          Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg)
         end
       | _ as tag -> (** Special treatment. TODO: use generic handler  *)
         Ftactic.nf_enter begin fun gl ->
@@ -1154,17 +1154,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               let (sigma,v) =
                 Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl
               in
-              Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v)
+              Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
           | OpenConstrArgType ->
               let (sigma,v) =
                 Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in
-              Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v)
+              Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
           | ConstrMayEvalArgType ->
               let (sigma,c_interp) =
                 interp_constr_may_eval ist env sigma
                   (out_gen (glbwit wit_constr_may_eval) x)
               in
-              Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp))
+              Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
           | ListArgType ConstrArgType ->
               let wit = glbwit (wit_list wit_constr) in
               let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
@@ -1173,7 +1173,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
                   (out_gen wit x)
                   (project gl)
               end gl in
-              Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp))
+              Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp))
           | ListArgType VarArgType ->
               let wit = glbwit (wit_list wit_var) in
               Ftactic.return (
@@ -1208,7 +1208,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               else
                 let goal = Proofview.Goal.goal gl in
                 let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
-                Ftactic.(lift (Proofview.V82.tclEVARS newsigma) <*> return v)
+                Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v)
           | _ -> assert false
         end
       in
@@ -1254,7 +1254,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
           Evd.MonadR.List.map_right
             (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
         in
-        Proofview.V82.tclEVARS sigma <*>
+        Proofview.Unsafe.tclEVARS sigma <*>
         catch_error_tac trace (tac args ist)
       end
 
@@ -1293,7 +1293,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
         let sigma = Proofview.Goal.sigma gl in
         let goal = Proofview.Goal.goal gl in
         let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
-        Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v)
+        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
       end
   | Reference r -> interp_ltac_reference dloc false ist r
   | ConstrMayEval c ->
@@ -1301,7 +1301,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
-        Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp))
+        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
       end
   | UConstr c ->
       Ftactic.enter begin fun gl ->
@@ -1335,7 +1335,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
         let (sigma,c_interp) =
           Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term
         in
-        Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp))
+        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
       end
   | TacNumgoals ->
       Ftactic.lift begin
@@ -1688,7 +1688,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
-        Proofview.V82.tclEVARS sigma <*> Tactics.intros_patterns l'
+        Proofview.Unsafe.tclEVARS sigma <*> Tactics.intros_patterns l'
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
@@ -1784,7 +1784,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
         let tac = Option.map (interp_tactic ist) t in
-        Proofview.V82.tclEVARS sigma <*> Tactics.forward b tac ipat c
+        Proofview.Unsafe.tclEVARS sigma <*> Tactics.forward b tac ipat c
       end
   | TacGeneralize cl ->
       let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
@@ -1792,7 +1792,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
-        Proofview.V82.tclEVARS sigma <*> tac cl
+        Proofview.Unsafe.tclEVARS sigma <*> tac cl
       end
   | TacGeneralizeDep c ->
       (new_interp_constr ist c)
@@ -1814,7 +1814,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
-	  Proofview.V82.tclEVARS sigma <*>
+	  Proofview.Unsafe.tclEVARS sigma <*>
             let_tac b (interp_fresh_name ist env sigma na) c_interp clp eqpat
         else
         (* We try to keep the pattern structure as much as possible *)
@@ -1992,7 +1992,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in
-        Proofview.V82.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps
+        Proofview.Unsafe.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Proofview.Goal.enter begin fun gl ->
@@ -2001,7 +2001,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let hyps = interp_hyp_list ist env sigma idl in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in
-        Proofview.V82.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps
+        Proofview.Unsafe.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.enter begin fun gl ->
@@ -2010,7 +2010,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,c_interp) = interp_constr ist env sigma c in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let hyps = interp_hyp_list ist env sigma idl in
-        Proofview.V82.tclEVARS sigma <*>
+        Proofview.Unsafe.tclEVARS sigma <*>
         Leminv.lemInv_clause dqhyps
           c_interp
           hyps
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 600ad86ef..2a21c53ab 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -494,7 +494,7 @@ module New = struct
           else
             tclUNIT ()
         in
-        Proofview.V82.tclEVARS sigma <*> tac x <*> check_evars_if
+        Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if
 
   let tclTIMEOUT n t =
     Proofview.tclOR
@@ -684,7 +684,7 @@ module New = struct
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
       let (sigma, c) = Evd.fresh_global env sigma ref in
-      Proofview.V82.tclEVARS sigma <*> (tac c)
+      Proofview.Unsafe.tclEVARS sigma <*> (tac c)
     end
 
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ea40fe4b9..83a3f2604 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -132,7 +132,7 @@ let convert_concl ?(check=true) ty k =
         sigma
       end else sigma in
     Tacticals.New.tclTHEN
-      (Proofview.V82.tclEVARS sigma)
+      (Proofview.Unsafe.tclEVARS sigma)
       (Proofview.Refine.refine ~unsafe:true (fun sigma ->
         let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ty in
         (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
@@ -155,7 +155,7 @@ let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
     try
       let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
-      Proofview.V82.tclEVARS sigma
+      Proofview.Unsafe.tclEVARS sigma
     with (* Reduction.NotConvertible *) _ ->
       (** FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
@@ -909,7 +909,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   let naming = NamingMustBe (dloc,targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
-    (Proofview.V82.tclEVARS clenv.evd)
+    (Proofview.Unsafe.tclEVARS clenv.evd)
     (if sidecond_first then
        Tacticals.New.tclTHENFIRST
          (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
@@ -1051,7 +1051,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
       build_case_analysis_scheme env sigma mind true sort
     else
       build_case_analysis_scheme_default env sigma mind sort in
-  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma)
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
   (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
     elimrename = Some (false, constructors_nrealdecls (fst mind))})
@@ -1090,7 +1090,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
     (Proofview.Goal.enter begin fun gl ->
       let evd, elim = find_eliminator c gl in
-	Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
+	Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd)
 	  (general_elim with_evars clear_flag cx elim)
     end)
     begin function
@@ -1266,7 +1266,7 @@ let solve_remaining_apply_goals =
       if Typeclasses.is_class_type sigma concl then
         let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in
 	Tacticals.New.tclTHEN
-          (Proofview.V82.tclEVARS evd')
+          (Proofview.Unsafe.tclEVARS evd')
           (Proofview.V82.tactic (refine_no_check c'))
 	else Proofview.tclUNIT ()
     with Not_found -> Proofview.tclUNIT ()
@@ -1460,7 +1460,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let sigma, c = f env sigma in
-      Proofview.V82.tclEVARS sigma <*>
+      Proofview.Unsafe.tclEVARS sigma <*>
 	(apply_in_once sidecond_first with_delta with_destruct with_evars naming id 
 	   (clear_flag,(loc,c)) tac)
   end
@@ -1518,7 +1518,7 @@ let exact_check c =
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let sigma, ct = Typing.e_type_of env sigma c in
-    Proofview.V82.tclEVARS sigma <*>
+    Proofview.Unsafe.tclEVARS sigma <*>
       Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
   end
 
@@ -1550,7 +1550,7 @@ let assumption =
         infer_conv env sigma t concl
     in
     if is_same_type then
-      (Proofview.V82.tclEVARS sigma) <*>
+      (Proofview.Unsafe.tclEVARS sigma) <*>
 	Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id))
     else arec gl only_eq rest
   in
@@ -1582,7 +1582,7 @@ let check_is_type env ty msg =
   let evdref = ref sigma in
   try
     let _ = Typing.sort_of env evdref ty in
-    Proofview.V82.tclEVARS !evdref
+    Proofview.Unsafe.tclEVARS !evdref
   with e when Errors.noncritical e ->
     msg e
 
@@ -1595,7 +1595,7 @@ let check_decl env (_, c, ty) msg =
     | None -> ()
     | Some c -> Typing.check env evdref c ty
     in
-    Proofview.V82.tclEVARS !evdref
+    Proofview.Unsafe.tclEVARS !evdref
   with e when Errors.noncritical e ->
     msg e
 
@@ -1739,7 +1739,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
 	
       let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
 	(Tacticals.New.tclTHENLIST
-           [Proofview.V82.tclEVARS sigma; 
+           [Proofview.Unsafe.tclEVARS sigma; 
 	    convert_concl_no_check redcl DEFAULTcast;
 	    intros; apply_tac])
   end
@@ -1993,7 +1993,7 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma,c = f env sigma in
-        Proofview.V82.tclEVARS sigma <*>
+        Proofview.Unsafe.tclEVARS sigma <*>
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
@@ -2143,11 +2143,11 @@ let letin_tac_gen with_eq abs ty =
       | None ->
 	  (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
     Tacticals.New.tclTHEN
-      (Proofview.V82.tclEVARUNIVCONTEXT ctx)
+      (Proofview.Unsafe.tclEVARUNIVCONTEXT ctx)
       (Proofview.Goal.nf_enter (fun gl -> 
 	let (sigma,newcl,eq_tac) = eq_tac gl in
 	  Tacticals.New.tclTHENLIST
-	    [ Proofview.V82.tclEVARS sigma;
+	    [ Proofview.Unsafe.tclEVARS sigma;
 	      convert_concl_no_check newcl DEFAULTcast;
               intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
               Tacticals.New.tclMAP convert_hyp_no_check depdecls;
@@ -2314,7 +2314,7 @@ let new_generalize_gen_let lconstr =
 	    generalize_goal_gen env ids i o t cl, args)
 	0 lconstr ((concl, sigma), [])
     in
-      Proofview.V82.tclEVARS sigma <*>
+      Proofview.Unsafe.tclEVARS sigma <*>
 	Proofview.Refine.refine begin fun sigma ->
           let (sigma, ev) = Evarutil.new_evar env sigma newcl in
             (sigma, (applist (ev, args)))
@@ -3497,7 +3497,7 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
   Proofview.Goal.nf_enter begin fun gl ->
   let (sigma, isrec, elim, indsign) = get_eliminator elim gl in
   let names = compute_induction_names (Array.length indsign) names in
-  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma)
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
   ((if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
     (Tacticals.New.tclTHEN
        (induct_tac elim)
@@ -3611,7 +3611,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbin
   Proofview.Goal.nf_enter begin fun gl ->
   let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
   Tacticals.New.tclTHENLIST
-    [Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0);
+    [Proofview.Unsafe.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0);
     (induction_from_context isrec with_evars elim_info
       (hyp0,lbind) names inhyps)]
   end
@@ -3631,7 +3631,7 @@ let induction_without_atomization isrec with_evars elim names lid =
   if not (Int.equal nlid awaited_nargs)
   then Tacticals.New.tclZEROMSG (str"Not the right number of induction arguments.")
   else
-    Proofview.tclTHEN (Proofview.V82.tclEVARS sigma)
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (induction_from_context_l with_evars elim_info lid names)
   end
 
@@ -3855,7 +3855,7 @@ let elim_type t =
   Proofview.Goal.enter begin fun gl ->
   let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
   let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
-  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t)
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t)
   end
 
 let case_type t =
@@ -3864,7 +3864,7 @@ let case_type t =
   let evd, elimc =
     Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl)
   in
-  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t)
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t)
   end
 
 
@@ -4125,7 +4125,7 @@ let abstract_subproof id gk tac =
     Entries.(snd (Future.force const.const_entry_body)) in
   let args = List.rev (instance_from_named_context sign) in
   let solve =
-    Proofview.V82.tclEVARS evd <*>
+    Proofview.Unsafe.tclEVARS evd <*>
     Proofview.tclEFFECTS effs <*>
     new_exact_no_check (applist (lem, args))
   in
@@ -4168,7 +4168,7 @@ let unify ?(state=full_transparent_state) x y =
       subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } }
     in
     let evd = w_unify (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) Reduction.CONV ~flags x y
-    in Proofview.V82.tclEVARS evd
+    in Proofview.Unsafe.tclEVARS evd
   with e when Errors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Not unifiable")
   end