diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-06 17:09:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-06 17:24:39 +0200 |
| commit | 521a7b96c8963428ca0ecb39a22f458bf603ccab (patch) | |
| tree | 4b96ec735f49ef1867348170b7432f9c7adb28bf /plugins/cc | |
| 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 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index e828345fa..45d6a9393 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -253,7 +253,7 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let type_of t = Tacmach.New.pf_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with @@ -321,7 +321,7 @@ let rec proof_tac p : unit Proofview.tactic = end let refute_tac c t1 t2 p = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl @@ -338,7 +338,7 @@ let refine_exact_check c gl = Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl @@ -353,7 +353,7 @@ let convert_to_goal_tac c t1 t2 p = end let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let tt2=constr_of_term t2 in let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in let false_t=mkApp (c2,[|mkVar h|]) in @@ -363,7 +363,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = end let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl @@ -404,7 +404,7 @@ let build_term_to_complete uf meta pac = applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (Pp.str "Reading subgoal ...") in let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in @@ -477,7 +477,7 @@ let congruence_tac depth l = *) let f_equal = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let type_of = Tacmach.New.pf_type_of gl in let cut_eq c1 c2 = |