Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.

1 files changed, 8 insertions, 9 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7453fff5c..14082bb8d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -112,13 +112,12 @@ open Auto
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
-      Proofview.V82.tactic
-	(fun gls ->
-	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
-	 tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+      let clenv' = clenv_unique_resolver ~flags clenv' gl in
+      Proofview.tclTHEN
+        (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+        (Tactics.Simple.eapply c)
     end }
 
 let hintmap_of sigma secvars hdc concl =
@@ -139,7 +138,7 @@ let e_exact poly flags (c,clenv) =
   end }
 
 let rec e_trivial_fail_db db_list local_db =
-  let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let next = Proofview.Goal.enter { enter = begin fun gl ->
     let d = Tacmach.New.pf_last_hyp gl in
     let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
     e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
@@ -149,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
@@ -501,7 +500,7 @@ let unfold_head env sigma (ids, csts) c =
   in aux c
 
 let autounfold_one db cl =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in