diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 | ||||
| -rw-r--r-- | proofs/clenv.mli | 3 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 12 | ||||
| -rw-r--r-- | proofs/logic.ml | 139 | ||||
| -rw-r--r-- | proofs/logic.mli | 6 | ||||
| -rw-r--r-- | proofs/refiner.ml | 14 | ||||
| -rw-r--r-- | proofs/refiner.mli | 30 |
7 files changed, 100 insertions, 108 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 37d54a4eea..08178052bf 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -321,10 +321,6 @@ let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = clenv_unify CUMUL ~flags (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv -let old_clenv_unique_resolver ?flags clenv gl = - let concl = Goal.V82.concl clenv.evd (sig_it gl) in - clenv_unique_resolver_gen ?flags clenv concl - let clenv_unique_resolver ?flags clenv gl = let concl = Proofview.Goal.concl gl in clenv_unique_resolver_gen ?flags clenv concl diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 1adfdb885a..4279ab4768 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -63,9 +63,6 @@ val clenv_unify : ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv (** unifies the concl of the goal with the type of the clenv *) -val old_clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv - val clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 767f93787d..c5e341c720 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -13,7 +13,6 @@ open Constr open Termops open Evd open EConstr -open Refiner open Logic open Reduction open Clenv @@ -61,10 +60,7 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv = clenv_pose_metas_as_evars clenv dep_mvs let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - (* ppedrot: a Goal.enter here breaks things, because the tactic below may - solve goals by side effects, while the compatibility layer keeps those - useless goals. That deserves a FIXME. *) - Proofview.V82.tactic begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then @@ -78,9 +74,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = else clenv.evd in let clenv = { clenv with evd = evd' } in - tclTHEN - (tclEVARS (Evd.clear_metas evd')) - (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) end let clenv_pose_dependent_evars ?(with_evars=false) clenv = diff --git a/proofs/logic.ml b/proofs/logic.ml index 406e71aafc..c7a1c32e7c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -28,16 +28,14 @@ module NamedDecl = Context.Named.Declaration type refiner_error = (* Errors raised by the refiner *) - | BadType of constr * constr * constr + | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * Evd.evar_map * refiner_error @@ -73,13 +71,11 @@ let catchable_exception = function let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) -(* Tells if the refiner should check that the submitted rules do not - produce invalid subgoals *) -let check = ref false -let with_check = Flags.with_option check +(* The check flag tells if the refiner should check that the submitted rules do + not produce invalid subgoals *) -let check_typability env sigma c = - if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma +let check_typability ~check env sigma c = + if check then fst (type_of env sigma (EConstr.of_constr c)) else sigma (************************************************************************) (************************************************************************) @@ -316,9 +312,9 @@ let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then raise (RefinerError (env, sigma, NonLinearProof c)) -let check_conv_leq_goal env sigma arg ty conclty = - if !check then - let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in +let check_conv_leq_goal ~check env sigma arg ty conclty = + if check then + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) conclty in match ans with | Some evm -> evm | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) @@ -334,28 +330,27 @@ let meta_free_prefix sigma a = in a with Stop acc -> Array.rev_of_list acc -let goal_type_of env sigma c = - if !check then +let goal_type_of ~check env sigma c = + if check then let (sigma,t) = type_of env sigma (EConstr.of_constr c) in (sigma, EConstr.Unsafe.to_constr t) else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) -let rec mk_refgoals sigma goal goalacc conclty trm = - let env = Goal.V82.env sigma goal in - let hyps = Goal.V82.hyps sigma goal in +let rec mk_refgoals ~check env sigma goalacc conclty trm = + let hyps = Environ.named_context_val env in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in - if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then + if (not check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in let t'ty = EConstr.Unsafe.to_constr t'ty in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else match kind trm with | Meta _ -> - let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in - if !check && occur_meta sigma conclty then + let conclty = nf_betaiota env sigma conclty in + if check && occur_meta sigma conclty then raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in @@ -363,9 +358,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> - let sigma = check_typability env sigma ty in - let sigma = check_conv_leq_goal env sigma trm ty conclty in - let res = mk_refgoals sigma goal goalacc ty t in + let sigma = check_typability ~check env sigma ty in + let sigma = check_conv_leq_goal ~check env sigma trm ty conclty in + let res = mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t in (* we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin @@ -388,24 +383,24 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let ty = EConstr.Unsafe.to_constr ty in goalacc, ty, sigma, f else - mk_hdgoals sigma goal goalacc f + mk_hdgoals ~check env sigma goalacc f in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in - let sigma = check_conv_leq_goal env sigma trm conclty' conclty in + let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in + let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in + let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in + let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -416,28 +411,27 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm."); - let (sigma, t'ty) = goal_type_of env sigma trm in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + let (sigma, t'ty) = goal_type_of ~check env sigma trm in + let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) (* Same as mkREFGOALS but without knowing the type of the term. Therefore, * Metas should be casted. *) -and mk_hdgoals sigma goal goalacc trm = - let env = Goal.V82.env sigma goal in - let hyps = Goal.V82.hyps sigma goal in +and mk_hdgoals ~check env sigma goalacc trm = + let hyps = Environ.named_context_val env in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> - let sigma = check_typability env sigma ty in + let sigma = check_typability ~check env sigma ty in let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> - let sigma = check_typability env sigma ty in - mk_refgoals sigma goal goalacc ty t + let sigma = check_typability ~check env sigma ty in + mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t | App (f,l) -> let (acc',hdty,sigma,applicand) = @@ -445,15 +439,15 @@ and mk_hdgoals sigma goal goalacc trm = then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) - else mk_hdgoals sigma goal goalacc f + else mk_hdgoals ~check env sigma goalacc f in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in + let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -462,21 +456,21 @@ and mk_hdgoals sigma goal goalacc trm = (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | _ -> - if !check && occur_meta sigma (EConstr.of_constr trm) then + if check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta."); - let (sigma, ty) = goal_type_of env sigma trm in + let (sigma, ty) = goal_type_of env ~check sigma trm in goalacc, ty, sigma, trm -and mk_arggoals sigma goal goalacc funty allargs = +and mk_arggoals ~check env sigma goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = whd_all env sigma (EConstr.of_constr funty) in let t = EConstr.Unsafe.to_constr t in let rec collapse t = match kind t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) @@ -485,19 +479,17 @@ and mk_arggoals sigma goal goalacc funty allargs = let t = collapse t in match kind t with | Prod (_, c1, b) -> - let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in + let (acc, hargty, sigma, arg) = mk_refgoals ~check env sigma goalacc (EConstr.of_constr c1) harg in (acc, subst1 harg b, sigma), arg | _ -> - let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs -and mk_casegoals sigma goal goalacc p c = - let env = Goal.V82.env sigma goal in - let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in +and mk_casegoals ~check env sigma goalacc p c = + let (acc',ct,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let ct = EConstr.of_constr ct in - let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in + let (acc'',pt,sigma,p') = mk_hdgoals ~check env sigma acc' p in let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals.") in @@ -505,20 +497,19 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') -and treat_case sigma goal ci lbrty lf acc' = +and treat_case ~check env sigma ci lbrty lf acc' = let rec strip_outer_cast c = match kind c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c in let decompose_app_vect c = match kind c with | App (f,cl) -> (f, cl) | _ -> (c,[||]) in - let env = Goal.V82.env sigma goal in Array.fold_left3 (fun (lacc,sigma,bacc) ty fi l -> if isMeta (strip_outer_cast fi) then (* Support for non-eta-let-expanded Meta as found in *) (* destruct/case with an non eta-let expanded elimination scheme *) - let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in + let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in r,s,(fi'::bacc) else (* Deal with a branch in expanded form of the form @@ -539,14 +530,14 @@ and treat_case sigma goal ci lbrty lf acc' = if isMeta head then begin assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); let head' = lift (-n) head in - let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in + let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in (r,s,fi'::bacc) end else (* Supposed to be meta-free *) - let sigma, t'ty = goal_type_of env sigma fi in - let sigma = check_conv_leq_goal env sigma fi t'ty ty in + let sigma, t'ty = goal_type_of ~check env sigma fi in + let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags @@ -574,18 +565,18 @@ let convert_hyp ~check ~reorder env sigma d = (************************************************************************) (* Primitive tactics are handled here *) -let prim_refiner r sigma goal = - let env = Goal.V82.env sigma goal in - let cl = Goal.V82.concl sigma goal in - let cl = EConstr.Unsafe.to_constr cl in +let refiner ~check r = + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let st = Proofview.Goal.state gl in + let cl = Proofview.Goal.concl gl in check_meta_variables env sigma r; - let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in - let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in - (sgl, sigma) - -let prim_refiner ~check r sigma goal = - if check then - with_check (prim_refiner r sigma) goal - else - prim_refiner r sigma goal + let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in + let map gl = Proofview.goal_with_state gl st in + let sgl = List.rev_map map sgl in + let sigma = Goal.V82.partial_solution env sigma (Proofview.Goal.goal gl) (EConstr.of_constr oterm) in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS sgl + end diff --git a/proofs/logic.mli b/proofs/logic.mli index ef8b2731b2..9dc75000a1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -26,23 +26,21 @@ open Evd (** The primitive refiner. *) -val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map +val refiner : check:bool -> constr -> unit Proofview.tactic (** {6 Refiner errors. } *) type refiner_error = (*i Errors raised by the refiner i*) - | BadType of constr * constr * constr + | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (*i Errors raised by the tactics i*) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * evar_map * refiner_error diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 75c3436cf4..874bab277d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -12,7 +12,6 @@ open Pp open CErrors open Util open Evd -open Logic type tactic = Proofview.V82.tac @@ -26,16 +25,7 @@ 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 refiner ~check pr goal_sigma = - let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in - { it = sgl; sigma = sigma'; } - -(* Profiling refiner *) -let refiner ~check = - if Flags.profile then - let refiner_key = CProfile.declare_profile "refiner" in - CProfile.profile2 refiner_key (refiner ~check) - else refiner ~check +let refiner = Logic.refiner (*********************) (* Tacticals *) @@ -269,5 +259,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = - tclEVARS (Evd.merge_universe_context (project gl) ctx) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 66eae1db81..a3cbfb5d5d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -22,49 +22,59 @@ 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 -> tactic +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 -val tclPUSHEVARUNIVCONTEXT : UState.t -> 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 @@ -72,15 +82,18 @@ val tclTHENS : tactic -> tactic list -> tactic 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 @@ -90,15 +103,28 @@ exception FailError of int * Pp.t Lazy.t 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."] |