diff options
Diffstat (limited to 'plugins/cc')
-rw-r--r-- | plugins/cc/cctac.ml | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0baa53370..09d9cf019 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -22,6 +22,7 @@ open Ccproof open Pp open Errors open Util +open Proofview.Notations let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -254,13 +255,13 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) let assert_before n c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) - end + end } let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with @@ -325,10 +326,10 @@ let rec proof_tac p : unit Proofview.tactic = app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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_unsafe_type_of gls tt1)) gl @@ -338,14 +339,14 @@ let refute_tac c t1 t2 p = let false_t=mkApp (c,[|mkVar hid|]) in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - end + end } let refine_exact_check c gl = let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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_unsafe_type_of gls tt2)) gl @@ -357,20 +358,20 @@ let convert_to_goal_tac c t1 t2 p = let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] - end + end } let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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 Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] - end + end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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_unsafe_type_of gls t1)) gl @@ -384,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p = let identity = Universes.constr_of_global (Lazy.force _I) in (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in let outtype = mkSort outtype in let pred=mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in @@ -399,7 +400,7 @@ let discriminate_tac (cstr,u as cstru) p = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) - end + end } (* wrap everything *) @@ -411,7 +412,7 @@ let build_term_to_complete uf meta pac = applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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 @@ -462,7 +463,7 @@ let cc_tactic depth additionnal_terms = convert_to_goal_tac id ta tb p | HeqnH (ida,idb) -> convert_to_hyp_tac ida ta idb tb p - end + end } let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") @@ -485,8 +486,7 @@ let congruence_tac depth l = let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> - Proofview.Goal.enter begin - fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in @@ -494,10 +494,10 @@ let mk_eq f c1 c2 k = let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) - end) + end }) let f_equal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) @@ -523,4 +523,4 @@ let f_equal = | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end - end + end } |