Removing the Change_evar refiner rule.

7 files changed, 9 insertions, 20 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 83a98745af..d682574779 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -17,7 +17,8 @@ open Locus
 
 (* The instantiate tactic *)
 
-let instantiate n (ist,rawc) ido gl =
+let instantiate_tac n (ist,rawc) ido =
+  Proofview.V82.tactic begin fun gl ->
   let sigma = gl.sigma in
   let evl =
     match ido with
@@ -44,14 +45,12 @@ let instantiate n (ist,rawc) ido gl =
     let filtered = Evd.evar_filtered_env evi in
     let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
     let sigma' = w_refine (evk,evi) ((constrvars, ist.Geninterp.lfun),rawc) sigma in
-      tclTHEN
-        (tclEVARS sigma')
-        tclNORMEVAR
-        gl
+    tclEVARS sigma' gl
+  end
 
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let sigma',evar = Evarutil.new_evar sigma env ~src typ in
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 0e653e5b7f..51ad3861df 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -11,7 +11,7 @@ open Names
 open Tacexpr
 open Locus
 
-val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
-  (Id.t * hyp_location_flag, unit) location -> tactic
+val instantiate_tac : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
+  (Id.t * hyp_location_flag, unit) location -> unit Proofview.tactic
 
 val let_evar : Name.t -> Term.types -> unit Proofview.tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 9ed9374476..28f8c2f402 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -434,8 +434,8 @@ open Tacticals
 
 TACTIC EXTEND instantiate
   [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] ->
-    [ Proofview.V82.tactic (instantiate i c hl)  ]
-| [ "instantiate" ] -> [ Proofview.V82.tactic (tclNORMEVAR) ]
+    [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ]
+| [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ]
 END
 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 27604d206d..82704c3c4e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -23,7 +23,6 @@ open Misctypes
 (* Tacticals re-exported from the Refiner module                        *)
 (************************************************************************)
 
-let tclNORMEVAR      = Refiner.tclNORMEVAR
 let tclIDTAC         = Refiner.tclIDTAC
 let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
 let tclORELSE0       = Refiner.tclORELSE0
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 8047281e89..46d62123cb 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -20,7 +20,6 @@ open Misctypes
 
 (** Tacticals i.e. functions from tactics to tactics. *)
 
-val tclNORMEVAR      : tactic
 val tclIDTAC         : tactic
 val tclIDTAC_MESSAGE : std_ppcmds -> tactic
 val tclORELSE0       : tactic -> tactic -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2926744ba8..28ca7edb57 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -676,13 +676,6 @@ let bring_hyps hyps =
       end
     end
 
-let resolve_classes gl =
-  let env = pf_env gl and evd = project gl in
-    if Evd.is_empty evd then tclIDTAC gl
-    else
-      let evd' = Typeclasses.resolve_typeclasses env evd in
-	(tclTHEN (tclEVARS evd') tclNORMEVAR) gl
-
 (**************************)
 (*     Cut tactics        *)
 (**************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9e10de8dda..0e92e7eb95 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -357,7 +357,6 @@ val generalize_gen  : ((occurrences * constr) * Name.t) list -> tactic
 val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> tactic
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
-val resolve_classes : tactic
 
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> tactic