diff options
| author | Pierre-Marie Pédrot | 2014-09-06 17:09:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-06 17:24:39 +0200 |
| commit | 521a7b96c8963428ca0ecb39a22f458bf603ccab (patch) | |
| tree | 4b96ec735f49ef1867348170b7432f9c7adb28bf /tactics/autorewrite.ml | |
| parent | 3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c (diff) | |
Renaming goal-entering functions.
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
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 0809c0500b..65166ec115 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) |