diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 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) |