From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- plugins/cc/cctac.ml | 44 +++++++++++++++++++++++--------------------- 1 file changed, 23 insertions(+), 21 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 5d894c677..c9c904e35 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -182,9 +182,10 @@ let litteral_of_constr env sigma term= (* store all equalities from the context *) let make_prb gls depth additionnal_terms = + let open Tacmach.New in let env=pf_env gls in - let sigma=sig_sig gls in - let state = empty depth gls in + let sigma=project gls in + let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter @@ -196,7 +197,7 @@ let make_prb gls depth additionnal_terms = let id = NamedDecl.get_id decl in begin let cid=Constr.mkVar id in - match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with + match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> @@ -213,7 +214,7 @@ let make_prb gls depth additionnal_terms = neg_hyps:=(cid,nh):: !neg_hyps | `Rule patts -> add_quant state id true patts | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); + end) (Proofview.Goal.hyps gls); begin match atom_of_constr env sigma (pf_concl gls) with `Eq (t,a,b) -> add_disequality state Goal a b @@ -227,6 +228,7 @@ let make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) let build_projection intype (cstr:pconstructor) special default gls= + let open Tacmach.New in let ci= (snd(fst cstr)) in let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in @@ -266,7 +268,7 @@ let refresh_universes ty k = let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.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 @@ -296,7 +298,7 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of tf1) (fun typf -> refresh_universes (type_of tx1) (fun typx -> refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> - let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in + let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in @@ -322,7 +324,7 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> let proj = - Tacmach.New.of_old (build_projection intype cstr special default) gl + build_projection intype cstr special default gl in let injt= app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in @@ -331,9 +333,9 @@ let rec proof_tac p : unit Proofview.tactic = end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in + let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in let k intype = let neweq= new_app_global _eq [|intype;tt1;tt2|] in @@ -347,12 +349,12 @@ 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.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = let neweq= new_app_global _eq [|sort;tt1;tt2|] in - let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in - let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in + let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity=mkLambda (Name x,sort,mkRel 1) in let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) @@ -361,9 +363,9 @@ let convert_to_goal_tac c t1 t2 p = end } let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.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 h = Tacmach.New.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; @@ -371,11 +373,11 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity = Universes.constr_of_global (Lazy.force _I) in let identity = EConstr.of_constr identity in let trivial = Universes.constr_of_global (Lazy.force _True) in @@ -385,8 +387,8 @@ let discriminate_tac (cstr,u as cstru) p = let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm 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 - let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in + let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in + let proj = build_projection intype cstru trivial concl gl in let injt=app_global _f_equal [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = @@ -409,11 +411,11 @@ let build_term_to_complete uf meta pac = applist (mkConstructU cinfo.ci_constr, all_args) let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (fun () -> Pp.str "Reading subgoal ...") in - let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in + let state = make_prb gl depth additionnal_terms in let _ = debug (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in let _ = debug (fun () -> Pp.str "Computation completed.") in @@ -498,7 +500,7 @@ let mk_eq f c1 c2 k = end }) let f_equal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = -- cgit v1.2.3