From b5155c528f91b97e5a799bcd07a3411281ea03d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 10 Nov 2021 14:02:02 +0100 Subject: [PATCH] Adapt w.r.t. coq/coq#15159. --- src/aac_rewrite.ml | 16 ++++++++-------- src/coq.ml | 22 +++++++++++----------- src/print.ml | 4 ++-- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/aac_rewrite.ml b/src/aac_rewrite.ml index 86fb3a6..a7a0edf 100644 --- a/src/aac_rewrite.ml +++ b/src/aac_rewrite.ml @@ -144,7 +144,7 @@ let by_aac_reflexivity zero <*> tclTac_or_exn apply_tac Coq.user_error (Pp.strbrk "unification failure") <*> tclTac_or_exn (time_tac "vm_norm" Tactics.normalise_in_concl) Coq.anomaly "vm_compute failure" <*> tclORELSE Tactics.reflexivity - (fun _ -> Tacticals.New.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) + (fun _ -> Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) @@ -169,7 +169,7 @@ let by_aac_normalise zero lift ir t t' = let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast in let apply_tac = Tactics.apply normalise_thm in - Tacticals.New.tclTHENLIST + Tacticals.tclTHENLIST [ Coq.tclRETYPE normalise_thm; Coq.tclRETYPE convert_to; convert ; apply_tac; @@ -202,12 +202,12 @@ let aac_normalise = let open Proofview.Notations in let open Proofview in Proofview.Goal.enter (fun goal -> - let ids = Tacmach.New.pf_ids_of_hyps goal in + let ids = Tacmach.pf_ids_of_hyps goal in let env = Proofview.Goal.env goal in tclEVARMAP >>= fun sigma -> let concl = Proofview.Goal.concl goal in let sigma,left,lift,ir,tleft,tright = aac_conclude env sigma concl in - Tacticals.New.tclTHENLIST + Tacticals.tclTHENLIST [ Unsafe.tclEVARS sigma; by_aac_normalise left lift ir tleft tright; @@ -273,7 +273,7 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equ right; |]) in - Tacticals.New.tclTHENLIST + Tacticals.tclTHENLIST [ Coq.tclRETYPE lift_transitivity; Tactics.apply lift_transitivity ] @@ -294,7 +294,7 @@ let core_aac_rewrite ?abort lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt in let rew = Coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst in - Tacticals.New.tclTHENS + Tacticals.tclTHENS (tclTac_or_exn (tran_tac) Coq.anomaly "Unable to make the transitivity step") ( if rewinfo.in_left @@ -344,7 +344,7 @@ let aac_rewrite_wrap ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict | Some (left, right, rlt) -> left,right,rlt in let check_type x = - Tacmach.New.pf_conv_x goal x rlt.Coq.Relation.carrier + Tacmach.pf_conv_x goal x rlt.Coq.Relation.carrier in let hypinfo = Coq.Rewrite.get_hypinfo env sigma ?check_type:(Some check_type) rew ~l2r in let sigma,rewinfo = dispatch env sigma in_left concl hypinfo in @@ -382,7 +382,7 @@ let aac_rewrite_wrap ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject with | NoSolutions -> - Tacticals.New.tclFAIL 0 + Tacticals.tclFAIL 0 (Pp.str (if occ_subterm = None && occ_sol = None then "No matching occurrence modulo AC found" else "No such solution")) diff --git a/src/coq.ml b/src/coq.ml index d7d75a3..15a71a2 100644 --- a/src/coq.ml +++ b/src/coq.ml @@ -48,7 +48,7 @@ let tclEVARS sigma gl = { it = [gl.it]; sigma } let retype c gl = - let sigma, _ = Tacmach.pf_apply Typing.type_of gl c in + let sigma, _ = Tacmach.Old.pf_apply Typing.type_of gl c in tclEVARS sigma gl (* similar to retype above. No Idea when/why this is needed, I smell some ugly hack. @@ -99,9 +99,9 @@ let cps_mk_letin : Proofview.V82.tac = fun goal -> let name = (Id.of_string name) in - let name = Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.pf_env goal) in + let name = Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.Old.pf_env goal) in let letin = (Proofview.V82.of_tactic (Tactics.letin_tac None (Name name) c None nowhere)) in - Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))] goal + Tacticals.Old.tclTHENLIST [retype c; letin; (k (mkVar name))] goal let mk_letin (name:string) (c: constr) : constr Proofview.tactic = let open Proofview.Notations in @@ -118,17 +118,17 @@ let mk_letin (name:string) (c: constr) : constr Proofview.tactic = type goal_sigma = Goal.goal Evd.sigma let goal_update (goal : goal_sigma) evar_map : goal_sigma = - let it = Tacmach.sig_it goal in - Tacmach.re_sig it evar_map + let it = Tacmach.Old.sig_it goal in + Tacmach.Old.re_sig it evar_map let resolve_one_typeclass goal ty : constr*goal_sigma= - let env = Tacmach.pf_env goal in - let evar_map = Tacmach.project goal in + let env = Tacmach.Old.pf_env goal in + let evar_map = Tacmach.Old.project goal in let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in c, (goal_update goal em) let cps_resolve_one_typeclass ?error : types -> (constr -> Proofview.V82.tac) -> Proofview.V82.tac = fun t k goal -> - Tacmach.pf_apply + Tacmach.Old.pf_apply (fun env em -> let em ,c = try Typeclasses.resolve_one_typeclass env em t with Not_found -> @@ -137,12 +137,12 @@ let cps_resolve_one_typeclass ?error : types -> (constr -> Proofview.V82.tac) - | Some x -> CErrors.user_err x end in - Tacticals.tclTHENLIST [tclEVARS em; k c] goal + Tacticals.Old.tclTHENLIST [tclEVARS em; k c] goal ) goal let nf_evar goal c : constr= - let evar_map = Tacmach.project goal in + let evar_map = Tacmach.Old.project goal in Evarutil.nf_evar evar_map c (* TODO: refactor following similar functions*) @@ -541,7 +541,7 @@ let rewrite ?(abort=false) hypinfo subst = ~with_evars:true (rew,Tactypes.NoBindings) else - Tacticals.New.tclIDTAC + Tacticals.tclIDTAC in tac diff --git a/src/print.ml b/src/print.ml index ab8c53f..f1e9e81 100644 --- a/src/print.ml +++ b/src/print.ml @@ -72,7 +72,7 @@ let print rlt ir m (context : EConstr.rel_context) : unit Proofview.tactic = if Search_monad.count m = 0 then ( - Tacticals.New.tclFAIL 0 (Pp.str "No subterm modulo AC") + Tacticals.tclFAIL 0 (Pp.str "No subterm modulo AC") ) else let _ = Feedback.msg_notice (Pp.str "All solutions:") in @@ -101,5 +101,5 @@ let print rlt ir m (context : EConstr.rel_context) : unit Proofview.tactic = (fun t -> Printer.pr_letype_env env sigma (Theory.Trans.raw_constr_of_t ir rlt context t)) m ) in - Tacticals.New.tclIDTAC + Tacticals.tclIDTAC