diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 0809c0500..65166ec11 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -91,7 +91,7 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tac (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in - let try_rewrite dir ctx c tc = Proofview.Goal.enter (fun gl -> + let try_rewrite dir ctx c tc = Proofview.Goal.nf_enter (fun gl -> let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in let sigma = Proofview.Goal.sigma gl in @@ -120,7 +120,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in let general_rewrite_in id = @@ -188,7 +188,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.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids end) |