Removing the Change_evar refiner rule.

13 files changed, 9 insertions, 41 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 0800374003..b16c8c502b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -654,12 +654,6 @@ let pr_prim_rule = function
   | Rename (id1,id2) ->
       (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
 
-  | Change_evars ->
-      (* This is internal tactic and cannot be replayed at user-level.
-         Function pr_rule_dot below is used when we want to hide
-         Change_evars *)
-      str "Evar change"
-
 
 (* Backwards compatibility *)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f283d0f339..30905e5771 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -713,8 +713,3 @@ let prim_refiner r sigma goal =
 	let ev = Vars.replace_vars [(id2,mkVar id1)] ev in
 	let sigma = Goal.V82.partial_solution sigma goal ev in
           ([gl], sigma)
-
-    | Change_evars ->
-	(* Normalises evars in goals. Used by instantiate. *)
-        let (goal,sigma) = Goal.V82.nf_evar sigma goal in
-	([goal],sigma)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 3ee7c87f77..f98bfa5ea2 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -39,7 +39,6 @@ type prim_rule =
   | Move of bool * Id.t * Id.t move_location
   | Order of Id.t list
   | Rename of Id.t * Id.t
-  | Change_evars
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 85ecfdd8a2..a5d6940770 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -31,7 +31,6 @@ type prim_rule =
   | Move of bool * Id.t * Id.t move_location
   | Order of Id.t list
   | Rename of Id.t * Id.t
-  | Change_evars
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6094287927..7e80b40e52 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -27,8 +27,6 @@ let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
   { it = sgl; sigma = sigma'; }
 
-let norm_evar_tac gl = refiner (Change_evars) gl
-
 (*********************)
 (*   Tacticals       *)
 (*********************)
@@ -47,9 +45,6 @@ let apply_sig_tac r tac g =
 (* [goal_goal_list : goal sigma -> goal list sigma] *)
 let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; }
 
-(* forces propagation of evar constraints *)
-let tclNORMEVAR = norm_evar_tac
-
 (* identity tactic without any message *)
 let tclIDTAC gls = goal_goal_list gls
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index db2c081d1b..012209410a 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -27,9 +27,6 @@ val refiner : rule -> tactic
 
 (** {6 Tacticals. } *)
 
-(** [tclNORMEVAR] forces propagation of evar constraints *)
-val tclNORMEVAR       : tactic
-
 (** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
 val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
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