diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c8fd0b7a75..8e296de617 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -162,7 +162,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | None -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids end) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9c5fdcd1ce..3456d13bbe 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -416,7 +416,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if get_typeclasses_filtered_unification () then let tac = matches_pattern concl p <*> - Proofview.Goal.nf_enter + Proofview.Goal.enter (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else diff --git a/tactics/equality.ml b/tactics/equality.ml index 0e39215701..d0f4b2c680 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -249,7 +249,7 @@ let rewrite_elim with_evars frzevars cls c e = let tclNOTSAMEGOAL tac = let goal gl = Proofview.Goal.goal gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let ev = goal gl in tac >>= fun () -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 95d545b046..6999b17d8e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2824,7 +2824,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let generalize_dep ?(with_let=false) c = let open Tacmach.New in let open Tacticals.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = pf_env gl in let sign = Proofview.Goal.hyps gl in let sigma = project gl in |