diff options
29 files changed, 288 insertions, 463 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9e04762d1e..819ad8a214 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -615,10 +615,11 @@ test-suite:4.11+trunk+dune: variables: OCAMLVER: 4.11.0+trunk -test-suite:4.12+trunk+dune: - extends: .test-suite:ocaml+beta+dune-template - variables: - OCAMLVER: 4.12.0+trunk +# Pending on https://github.com/ocaml/dune/pull/3585 +# test-suite:4.12+trunk+dune: +# extends: .test-suite:ocaml+beta+dune-template +# variables: +# OCAMLVER: 4.12.0+trunk test-suite:base+async: extends: .test-suite-template diff --git a/dev/base_include b/dev/base_include index 67ea3a1fa1..1f14fc2941 100644 --- a/dev/base_include +++ b/dev/base_include @@ -114,7 +114,6 @@ open Logic open Proof open Proof_using open Redexpr -open Refiner open Tacmach open Hints diff --git a/dev/ci/ci-coq_performance_tests.sh b/dev/ci/ci-coq_performance_tests.sh index 4eb77cfb24..fde8df8e3d 100755 --- a/dev/ci/ci-coq_performance_tests.sh +++ b/dev/ci/ci-coq_performance_tests.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download coq_performance_tests -( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf && make validate && make install ) +( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf-Sanity && make validate && make install ) diff --git a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh new file mode 100644 index 0000000000..c8c5b3ed5a --- /dev/null +++ b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12599" ] || [ "$CI_BRANCH" = "rm-deprecated-refiner" ]; then + + equations_CI_REF=rm-deprecated-refiner + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index bca1eb5754..f14edec639 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -186,7 +186,7 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) -let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g)) +let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Tacmach.project g)) let pphintdb db = pp(envpp Hints.pr_hint_db_env db) let ppproofview p = let gls,sigma = Proofview.proofview p in diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 8427300dc4..e5c2056c40 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -55,6 +55,10 @@ Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. +Erik Martin-Dorel has maintained the `Coq Docker images +<https://hub.docker.com/r/coqorg/coq>`_ that are used in many Coq +projects for continuous integration. + The OPAM repository for |Coq| packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 2151ad7873..9b578d4697 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -43,7 +43,7 @@ let finish_proof dynamic_infos g = let refine c = Proofview.V82.of_tactic - (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)) + (Logic.refiner ~check:true EConstr.Unsafe.(to_constr c)) let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index f16d0717df..40dea90c00 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1567,7 +1567,7 @@ let assert_replacing id newt tac = let newfail n s = let info = Exninfo.reify () in - Proofview.tclZERO ~info (Refiner.FailError (n, lazy s)) + Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s)) let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in @@ -1656,7 +1656,7 @@ let cl_rewrite_clause_strat progress strat clause = (fun (e, info) -> match e with | RewriteFailure e -> tclZEROMSG ~info (str"setoid rewrite failed: " ++ e) - | Refiner.FailError (n, pp) -> + | Tacticals.FailError (n, pp) -> tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) | e -> Proofview.tclZERO ~info e)) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 705a1a62ce..fdebe14a23 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -22,7 +22,6 @@ open Util open Names open Nameops open Libnames -open Refiner open Tacmach.New open Tactic_debug open Constrexpr @@ -1103,8 +1102,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> Proofview.V82.tactic begin - tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) - end [@ocaml.warning "-3"] + Tacticals.tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) + end | TacAbstract (t,ido) -> let call = LtacMLCall tac in let trace = push_trace(None,call) ist in @@ -1442,6 +1441,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = if the left-hand side fails. *) and interp_match_successes lz ist s = let general = + let open Tacticals in let break (e, info) = match e with | FailError (0, _) -> None | FailError (n, s) -> Some (FailError (pred n, s), info) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e7c75e029e..878f7a834e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -201,7 +201,7 @@ let exec_tactic env evd n f args = (* Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd = Evd.minimize_universes (Refiner.project gls) in + let evd = Evd.minimize_universes gls.Evd.sigma in let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 01e8daf82d..5f463f8de4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0 (* }}} *) let pf_merge_uc uc gl = - re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc) + re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc) let pf_merge_uc_of sigma gl = let ucst = Evd.evar_universe_context sigma in pf_merge_uc ucst gl @@ -1029,7 +1029,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t = pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Proofview.(V82.of_tactic (Tacticals.New.tclTHENLIST [ - Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t); + Logic.refiner ~check:false EConstr.Unsafe.(to_constr t); (if first_goes_last then cycle 1 else tclUNIT ()) ])) gl end diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 8e75ba7a2b..a12b4aad11 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -482,7 +482,7 @@ let revtoptac n0 = let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) + Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) end let equality_inj l b id c = diff --git a/printing/printer.ml b/printing/printer.ml index b0a4c8b738..96213b3b8b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -16,7 +16,6 @@ open Constr open Context open Environ open Evd -open Refiner open Constrextern open Ppconstr open Declarations @@ -453,7 +452,7 @@ let pr_transparent_state ts = *) let pr_goal ?(diffs=false) ?og_s g_s = let g = sig_it g_s in - let sigma = project g_s in + let sigma = Tacmach.project g_s in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index c78cc96a83..43f70dfecc 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -335,7 +335,7 @@ let unwrap g_s = match g_s with | Some g_s -> let goal = Evd.sig_it g_s in - let sigma = Refiner.project g_s in + let sigma = Tacmach.project g_s in goal_info goal sigma | None -> ([], CString.Map.empty, Pp.mt ()) @@ -545,7 +545,7 @@ let match_goals ot nt = let get_proof_context (p : Proof.t) = let Proof.{goals; sigma} = Proof.data p in - sigma, Refiner.pf_env { Evd.it = List.(hd goals); sigma } + sigma, Tacmach.pf_env { Evd.it = List.(hd goals); sigma } let to_constr pf = let open CAst in diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 790a9dd2cc..5f19c1bb09 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,6 +6,5 @@ Proof Logic Goal_select Proof_bullet -Refiner Tacmach Clenv diff --git a/proofs/refiner.ml b/proofs/refiner.ml deleted file mode 100644 index 874bab277d..0000000000 --- a/proofs/refiner.ml +++ /dev/null @@ -1,261 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Evd - -type tactic = Proofview.V82.tac - -module NamedDecl = Context.Named.Declaration - -let sig_it x = x.it -let project x = x.sigma - -(* Getting env *) - -let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) -let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) - -let refiner = Logic.refiner - -(*********************) -(* Tacticals *) -(*********************) - - -let unpackage glsig = (ref (glsig.sigma)), glsig.it - -let repackage r v = {it = v; sigma = !r; } - -let apply_sig_tac r tac g = - Control.check_for_interrupt (); (* Breakpoint *) - let glsigma = tac (repackage r g) in - r := glsigma.sigma; - glsigma.it - -(* [goal_goal_list : goal sigma -> goal list sigma] *) -let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } - -(* identity tactic without any message *) -let tclIDTAC gls = goal_goal_list gls - -(* the message printing identity tactic *) -let tclIDTAC_MESSAGE s gls = - Feedback.msg_info (hov 0 s); tclIDTAC gls - -(* General failure tactic *) -let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) - -(* A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.t Lazy.t - -(* The Fail tactic *) -let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) - -let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) - -let start_tac gls = - let sigr, g = unpackage gls in - (sigr, [g]) - -let finish_tac (sigr,gl) = repackage sigr gl - -(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last - m subgoals, and [tac] on the others *) -let thens3parts_tac tacfi tac tacli (sigr,gs) = - let nf = Array.length tacfi in - let nl = Array.length tacli in - let ng = List.length gs in - if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals."); - let gll = - (List.map_i (fun i -> - apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) - 0 gs) in - (sigr,List.flatten gll) - -(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) -let thensf_tac taci tac = thens3parts_tac taci tac [||] - -(* Apply [tac i] on the ith subgoal (no subgoals number check) *) -let thensi_tac tac (sigr,gs) = - let gll = - List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in - (sigr, List.flatten gll) - -let then_tac tac = thensf_tac [||] tac - -(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] - applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to - the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] - subgoals and [tac2] to the rest of the subgoals in the middle. Raises an - error if the number of resulting subgoals is strictly less than [n+m] *) -let tclTHENS3PARTS tac1 tacfi tac tacli gls = - finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls))) - -(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1] - to [gls] and applies [t1], ..., [tn] to the first [n] resulting - subgoals, and [tac2] to the others subgoals. Raises an error if - the number of resulting subgoals is strictly less than [n] *) -let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||] - -(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] - to [gls] and applies [t1], ..., [tn] to the last [n] resulting - subgoals, and [tac2] to the other subgoals. Raises an error if the - number of resulting subgoals is strictly less than [n] *) -let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci - -(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies - [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the - number of subgoals is *) -let tclTHEN_i tac taci gls = - finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) - -(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [tac2] to every resulting subgoals *) -let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] - -(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to - [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises - an error if the number of resulting subgoals is not [n] *) -let tclTHENSV tac1 tac2v = - tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||] - -let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) - -(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the last resulting subgoal *) -let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] - -(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the first resulting subgoal *) -let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC - -(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More - convenient than [tclTHEN] when [n] is large. *) -let rec tclTHENLIST = function - [] -> tclIDTAC - | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) - -(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) -let tclMAP tacfun l = - List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC - -(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves -the goal unchanged *) -let tclPROGRESS tac ptree = - let rslt = tac ptree in - if Goal.V82.progress rslt ptree then rslt - else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") - -(* Execute tac, show the names of new hypothesis names created by tac - in the "as" format and then forget everything. From the logical - point of view [tclSHOWHYPS tac] is therefore equivalent to idtac, - except that it takes the time and memory of tac and prints "as" - information). The resulting (unchanged) goals are printed *after* - the as-expression, which forces pg to some gymnastic. - TODO: Have something similar (better?) in the xml protocol. - NOTE: some tactics delete hypothesis and reuse names (induction, - destruct), this is not detected by this tactical. *) -let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) - : Goal.goal list Evd.sigma = - let oldhyps = pf_hyps goal in - let rslt:Goal.goal list Evd.sigma = tac goal in - let { it = gls; sigma = sigma; } = rslt in - let hyps = - List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in - let newhyps = - List.map - (fun hypl -> List.subtract cmp hypl oldhyps) - hyps - in - let s = - let frst = ref true in - List.fold_left - (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") - ^ (List.fold_left - (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) - "" lh)) - "" newhyps in - Feedback.msg_notice - (str "<infoH>" - ++ (hov 0 (str s)) - ++ (str "</infoH>")); - tclIDTAC goal;; - - -let catch_failerror (e, info) = - match e with - | FailError (lvl,s) when lvl > 0 -> - Exninfo.iraise (FailError (lvl - 1, s), info) - | e -> Control.check_for_interrupt () - -(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) -let tclORELSE0 t1 t2 g = - try - t1 g - with (* Breakpoint *) - | e when CErrors.noncritical e -> - let e = Exninfo.capture e in catch_failerror e; t2 g - -(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, - then applies t2 *) -let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 - -(* applies t1;t2then if t1 succeeds or t2else if t1 fails - t2* are called in terminal position (unless t1 produces more than - 1 subgoal!) *) -let tclORELSE_THEN t1 t2then t2else gls = - match - try Some(tclPROGRESS t1 gls) - with e when CErrors.noncritical e -> - let e = Exninfo.capture e in catch_failerror e; None - with - | None -> t2else gls - | Some sgl -> - let sigr, gl = unpackage sgl in - finish_tac (then_tac t2then (sigr,gl)) - -(* TRY f tries to apply f, and if it fails, leave the goal unchanged *) -let tclTRY f = (tclORELSE0 f tclIDTAC) - -let tclTHENTRY f g = (tclTHEN f (tclTRY g)) - -(* Try the first tactic that does not fail in a list of tactics *) - -let rec tclFIRST = function - | [] -> tclFAIL_s "No applicable tactic." - | t::rest -> tclORELSE0 t (tclFIRST rest) - -(* Fails if a tactic did not solve the goal *) -let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") - -(* Iteration tacticals *) - -let tclDO n t = - let rec dorec k = - if k < 0 then user_err ~hdr:"Refiner.tclDO" - (str"Wrong argument : Do needs a positive integer."); - if Int.equal k 0 then tclIDTAC - else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) - in - dorec n - - -(* Beware: call by need of CAML, g is needed *) -let rec tclREPEAT t g = - tclORELSE_THEN t (tclREPEAT t) tclIDTAC g - -let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) - -(* Change evars *) -let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} diff --git a/proofs/refiner.mli b/proofs/refiner.mli deleted file mode 100644 index a3cbfb5d5d..0000000000 --- a/proofs/refiner.mli +++ /dev/null @@ -1,130 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Legacy proof engine. Do not use in newly written code. *) - -open Evd -open EConstr - -(** The refiner (handles primitive rules and high-level tactics). *) -type tactic = Proofview.V82.tac - -val sig_it : 'a sigma -> 'a -val project : 'a sigma -> evar_map - -val pf_env : Goal.goal sigma -> Environ.env -val pf_hyps : Goal.goal sigma -> named_context - -val refiner : check:bool -> Constr.t -> unit Proofview.tactic - -(** {6 Tacticals. } *) - -(** [tclIDTAC] is the identity tactic without message printing*) -val tclIDTAC : tactic -[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"] -val tclIDTAC_MESSAGE : Pp.t -> tactic -[@@ocaml.deprecated] - -(** [tclEVARS sigma] changes the current evar map *) -val tclEVARS : evar_map -> tactic -[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"] - - -(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [tac2] to every resulting subgoals *) -val tclTHEN : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHEN"] - -(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More - convenient than [tclTHEN] when [n] is large *) -val tclTHENLIST : tactic list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"] - -(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) -val tclMAP : ('a -> tactic) -> 'a list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclMAP"] - -(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *) -val tclTHEN_i : tactic -> (int -> tactic) -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"] - -(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the last resulting subgoal (previously called [tclTHENL]) *) -val tclTHENLAST : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"] - -(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the first resulting subgoal *) -val tclTHENFIRST : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"] - -(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to - [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises - an error if the number of resulting subgoals is not [n] *) -val tclTHENSV : tactic -> tactic array -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"] - -(** Same with a list of tactics *) -val tclTHENS : tactic -> tactic list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENS"] - -(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] - applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to - the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] - subgoals and [tac2] to the rest of the subgoals in the middle. Raises an - error if the number of resulting subgoals is strictly less than [n+m] *) -val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"] - -(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the - last [n] resulting subgoals and [tac2] on the remaining first subgoals *) -val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"] - -(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then - applies [t1],...,[tn] on the first [n] resulting subgoals and - [tac2] for the remaining last subgoals (previously called tclTHENST) *) -val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"] - -(** A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.t Lazy.t - -(** Takes an exception and either raise it at the next - level or do nothing. *) -val catch_failerror : Exninfo.iexn -> unit - -val tclORELSE0 : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"] -val tclORELSE : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclORELSE"] -val tclREPEAT : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"] -val tclFIRST : tactic list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclFIRST"] -val tclTRY : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTRY"] -val tclTHENTRY : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"] -val tclCOMPLETE : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"] -val tclAT_LEAST_ONCE : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"] -val tclFAIL : int -> Pp.t -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclFAIL"] -val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"] -val tclDO : int -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclDO"] -val tclPROGRESS : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"] -val tclSHOWHYPS : tactic -> tactic -[@@ocaml.deprecated "Internal tactic. Do not use."] diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0bac0b0424..ecdbfa5118 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -29,10 +29,10 @@ let re_sig it gc = { it = it; sigma = gc; } type tactic = Proofview.V82.tac -let sig_it = Refiner.sig_it -let project = Refiner.project -let pf_env = Refiner.pf_env -let pf_hyps = Refiner.pf_hyps +let sig_it x = x.it +let project x = x.sigma +let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) +let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) let test_conversion env sigma pb c1 c2 = Reductionops.check_conv ~pb env sigma c1 c2 diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4156d5f0ee..82ce2234e3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1183,7 +1183,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = try Proofview.V82.of_tactic (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls - with Refiner.FailError _ -> raise Not_found + with Tacticals.FailError _ -> raise Not_found in let evd = sig_sig gls' in let t' = mkEvar (ev, subst) in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index d275e15255..686303a2ab 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -206,7 +206,7 @@ module SearchProblem = struct (ngls, lgls, cost, pptac) :: aux tacl with e when CErrors.noncritical e -> let e = Exninfo.capture e in - Refiner.catch_failerror e; aux tacl + Tacticals.catch_failerror e; aux tacl in aux l (* Ordering of states is lexicographic on depth (greatest first) then diff --git a/tactics/equality.ml b/tactics/equality.ml index 39017c946f..3aa7626aaa 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1047,7 +1047,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) - [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] + [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1366,7 +1366,7 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + Logic.refiner ~check:true EConstr.Unsafe.(to_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> @@ -1412,7 +1412,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)]) + Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 22c5bbe73f..d5358faf59 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -23,39 +23,236 @@ open Tactypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -(************************************************************************) -(* Tacticals re-exported from the Refiner module *) -(************************************************************************) +(*********************) +(* Tacticals *) +(*********************) type tactic = Proofview.V82.tac -[@@@ocaml.warning "-3"] - -let tclIDTAC = Refiner.tclIDTAC -let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE -let tclORELSE0 = Refiner.tclORELSE0 -let tclORELSE = Refiner.tclORELSE -let tclTHEN = Refiner.tclTHEN -let tclTHENLIST = Refiner.tclTHENLIST -let tclMAP = Refiner.tclMAP -let tclTHEN_i = Refiner.tclTHEN_i -let tclTHENFIRST = Refiner.tclTHENFIRST -let tclTHENLAST = Refiner.tclTHENLAST -let tclTHENS = Refiner.tclTHENS -let tclTHENSV = Refiner.tclTHENSV -let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn -let tclTHENSLASTn = Refiner.tclTHENSLASTn -let tclREPEAT = Refiner.tclREPEAT -let tclFIRST = Refiner.tclFIRST -let tclTRY = Refiner.tclTRY -let tclCOMPLETE = Refiner.tclCOMPLETE -let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE -let tclFAIL = Refiner.tclFAIL -let tclFAIL_lazy = Refiner.tclFAIL_lazy -let tclDO = Refiner.tclDO -let tclPROGRESS = Refiner.tclPROGRESS -let tclSHOWHYPS = Refiner.tclSHOWHYPS -let tclTHENTRY = Refiner.tclTHENTRY +open Evd + +exception FailError of int * Pp.t Lazy.t + +let catch_failerror (e, info) = + match e with + | FailError (lvl,s) when lvl > 0 -> + Exninfo.iraise (FailError (lvl - 1, s), info) + | e -> Control.check_for_interrupt () + +let unpackage glsig = (ref (glsig.sigma)), glsig.it + +let repackage r v = {it = v; sigma = !r; } + +let apply_sig_tac r tac g = + Control.check_for_interrupt (); (* Breakpoint *) + let glsigma = tac (repackage r g) in + r := glsigma.sigma; + glsigma.it + +(* [goal_goal_list : goal sigma -> goal list sigma] *) +let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } + +(* identity tactic without any message *) +let tclIDTAC gls = goal_goal_list gls + +(* the message printing identity tactic *) +let tclIDTAC_MESSAGE s gls = + Feedback.msg_info (hov 0 s); tclIDTAC gls + +(* General failure tactic *) +let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) + +(* The Fail tactic *) +let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) + +let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) + +let start_tac gls = + let sigr, g = unpackage gls in + (sigr, [g]) + +let finish_tac (sigr,gl) = repackage sigr gl + +(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last + m subgoals, and [tac] on the others *) +let thens3parts_tac tacfi tac tacli (sigr,gs) = + let nf = Array.length tacfi in + let nl = Array.length tacli in + let ng = List.length gs in + if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals."); + let gll = + (List.map_i (fun i -> + apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) + 0 gs) in + (sigr,List.flatten gll) + +(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) +let thensf_tac taci tac = thens3parts_tac taci tac [||] + +(* Apply [tac i] on the ith subgoal (no subgoals number check) *) +let thensi_tac tac (sigr,gs) = + let gll = + List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in + (sigr, List.flatten gll) + +let then_tac tac = thensf_tac [||] tac + +(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] + applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to + the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] + subgoals and [tac2] to the rest of the subgoals in the middle. Raises an + error if the number of resulting subgoals is strictly less than [n+m] *) +let tclTHENS3PARTS tac1 tacfi tac tacli gls = + finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls))) + +(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the first [n] resulting + subgoals, and [tac2] to the others subgoals. Raises an error if + the number of resulting subgoals is strictly less than [n] *) +let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||] + +(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the last [n] resulting + subgoals, and [tac2] to the other subgoals. Raises an error if the + number of resulting subgoals is strictly less than [n] *) +let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci + +(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies + [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the + number of subgoals is *) +let tclTHEN_i tac taci gls = + finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] + +(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to + [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises + an error if the number of resulting subgoals is not [n] *) +let tclTHENSV tac1 tac2v = + tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||] + +let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) + +(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal *) +let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] + +(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the first resulting subgoal *) +let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC + +(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More + convenient than [tclTHEN] when [n] is large. *) +let rec tclTHENLIST = function + [] -> tclIDTAC + | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) + +(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +let tclMAP tacfun l = + List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC + +(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves +the goal unchanged *) +let tclPROGRESS tac ptree = + let rslt = tac ptree in + if Goal.V82.progress rslt ptree then rslt + else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") + +(* Execute tac, show the names of new hypothesis names created by tac + in the "as" format and then forget everything. From the logical + point of view [tclSHOWHYPS tac] is therefore equivalent to idtac, + except that it takes the time and memory of tac and prints "as" + information). The resulting (unchanged) goals are printed *after* + the as-expression, which forces pg to some gymnastic. + TODO: Have something similar (better?) in the xml protocol. + NOTE: some tactics delete hypothesis and reuse names (induction, + destruct), this is not detected by this tactical. *) +let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) + : Goal.goal list Evd.sigma = + let oldhyps = pf_hyps goal in + let rslt:Goal.goal list Evd.sigma = tac goal in + let { it = gls; sigma = sigma; } = rslt in + let hyps = + List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in + let newhyps = + List.map + (fun hypl -> List.subtract cmp hypl oldhyps) + hyps + in + let s = + let frst = ref true in + List.fold_left + (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") + ^ (List.fold_left + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) + "" lh)) + "" newhyps in + Feedback.msg_notice + (str "<infoH>" + ++ (hov 0 (str s)) + ++ (str "</infoH>")); + tclIDTAC goal;; + +(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) +let tclORELSE0 t1 t2 g = + try + t1 g + with (* Breakpoint *) + | e when CErrors.noncritical e -> + let e = Exninfo.capture e in catch_failerror e; t2 g + +(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, + then applies t2 *) +let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 + +(* applies t1;t2then if t1 succeeds or t2else if t1 fails + t2* are called in terminal position (unless t1 produces more than + 1 subgoal!) *) +let tclORELSE_THEN t1 t2then t2else gls = + match + try Some(tclPROGRESS t1 gls) + with e when CErrors.noncritical e -> + let e = Exninfo.capture e in catch_failerror e; None + with + | None -> t2else gls + | Some sgl -> + let sigr, gl = unpackage sgl in + finish_tac (then_tac t2then (sigr,gl)) + +(* TRY f tries to apply f, and if it fails, leave the goal unchanged *) +let tclTRY f = (tclORELSE0 f tclIDTAC) + +let tclTHENTRY f g = (tclTHEN f (tclTRY g)) + +(* Try the first tactic that does not fail in a list of tactics *) + +let rec tclFIRST = function + | [] -> tclFAIL_s "No applicable tactic." + | t::rest -> tclORELSE0 t (tclFIRST rest) + +(* Fails if a tactic did not solve the goal *) +let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") + +(* Iteration tacticals *) + +let tclDO n t = + let rec dorec k = + if k < 0 then user_err ~hdr:"Refiner.tclDO" + (str"Wrong argument : Do needs a positive integer."); + if Int.equal k 0 then tclIDTAC + else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) + in + dorec n + + +(* Beware: call by need of CAML, g is needed *) +let rec tclREPEAT t g = + tclORELSE_THEN t (tclREPEAT t) tclIDTAC g + +let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (************************************************************************) (* Tacticals applying on hypotheses *) @@ -245,10 +442,12 @@ let elimination_sort_of_clause = function | None -> elimination_sort_of_goal | Some id -> elimination_sort_of_hyp id +(* Change evars *) +let tclEVARS sigma gls = tclIDTAC {gls with Evd.sigma=sigma} let pf_with_evars glsev k gls = let evd, a = glsev gls in - tclTHEN (Refiner.tclEVARS evd) (k a) gls + tclTHEN (tclEVARS evd) (k a) gls let pf_constr_of_global gr k = pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k @@ -271,7 +470,7 @@ module New = struct | None -> Exninfo.reify () | Some info -> info in - tclZERO ~info (Refiner.FailError (lvl,lazy msg)) + tclZERO ~info (FailError (lvl,lazy msg)) let tclZEROMSG ?info ?loc msg = let info = match info with @@ -289,7 +488,7 @@ module New = struct let catch_failerror e = try - Refiner.catch_failerror e; + catch_failerror e; tclUNIT () with e when CErrors.noncritical e -> let _, info = Exninfo.capture e in @@ -320,7 +519,7 @@ module New = struct let tclONCE = Proofview.tclONCE - let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t + let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (FailError(0,lazy (assert false))) t let tclIFCATCH t tt te = tclINDEPENDENT begin @@ -570,7 +769,7 @@ module New = struct begin function (e, info) -> match e with | Logic_monad.Tac_Timeout as e -> let info = Exninfo.reify () in - Proofview.tclZERO ~info (Refiner.FailError (0,lazy (CErrors.print e))) + Proofview.tclZERO ~info (FailError (0,lazy (CErrors.print e))) | e -> Proofview.tclZERO ~info e end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 88419af836..48a06e6e1d 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -15,6 +15,13 @@ open Evd open Locus open Tactypes +(** A special exception for levels for the Fail tactic *) +exception FailError of int * Pp.t Lazy.t + +(** Takes an exception and either raise it at the next + level or do nothing. *) +val catch_failerror : Exninfo.iexn -> unit + (** Tacticals i.e. functions from tactics to tactics. *) type tactic = Proofview.V82.tac diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3133f9be1e..af23747d43 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -30,7 +30,6 @@ open Genredexpr open Tacmach.New open Logic open Clenv -open Refiner open Tacticals open Hipattern open Coqlib @@ -355,7 +354,7 @@ let fresh_id_in_env avoid id env = next_ident_away_in_goal id avoid let fresh_id avoid id gl = - fresh_id_in_env avoid id (pf_env gl) + fresh_id_in_env avoid id (Tacmach.pf_env gl) let new_fresh_id avoid id gl = fresh_id_in_env avoid id (Proofview.Goal.env gl) @@ -1007,7 +1006,7 @@ let find_intro_names ctxt gl = let name = fresh_id avoid (default_id env gl.sigma decl) gl in let newenv = push_rel decl env in (newenv, name :: idl, Id.Set.add name avoid)) - ctxt (pf_env gl, [], Id.Set.empty) in + ctxt (Tacmach.pf_env gl, [], Id.Set.empty) in List.rev res let build_intro_tac id dest tac = match dest with @@ -1383,7 +1382,7 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = if not with_evars && occur_meta clenv.evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in + let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 66305dfefa..563651cfa5 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-async-proofs" "off") *) Module applydestruct. Class Foo (A : Type) := { bar : nat -> A; diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 62a66daf7d..98e2917300 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-async-proofs" "off") *) (* Wish #2154 by E. van der Weegen *) (* auto was not using f_equal-style lemmas with metavariables occurring diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index cea7d92c0b..9577d63f61 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-async-proofs" "off") *) Require Import Program.Tactics. Module Backtracking. Class A := { foo : nat }. diff --git a/vernac/declare.ml b/vernac/declare.ml index 6326a22e83..85359d5b62 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -2206,7 +2206,7 @@ let solve_by_tac ?loc name evi t ~poly ~uctx = Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body); Some (body, types, uctx) with - | Refiner.FailError (_, s) as exn -> + | Tacticals.FailError (_, s) as exn -> let _ = Exninfo.capture exn in CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) (* If the proof is open we absorb the error and leave the obligation open *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 540d470fdc..0c4f76f682 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1398,7 +1398,7 @@ let rec vernac_interp_error_handler = function str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment." - | Refiner.FailError (i,s) -> + | Tacticals.FailError (i,s) -> let s = Lazy.force s in str "Tactic failure" ++ (if Pp.ismt s then s else str ": " ++ s) ++ |