diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 8 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 35 | ||||
| -rw-r--r-- | tactics/eqschemes.mli | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 24 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 105 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 24 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
9 files changed, 124 insertions, 84 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 910e042e7a..9a517652a7 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -27,11 +27,11 @@ open Ind_tables let optimize_non_type_induction_scheme kind dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - if check_scheme kind ind then + match lookup_scheme kind ind with + | Some cte -> (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the appropriate type *) - let cte = lookup_scheme kind ind in let sigma, cte = Evd.fresh_constant_instance env sigma cte in let c = mkConstU cte in let t = type_of_constant_in (Global.env()) cte in @@ -48,7 +48,7 @@ let optimize_non_type_induction_scheme kind dep sort ind = let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) - else + | None -> let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma) @@ -62,7 +62,7 @@ let build_induction_scheme_in_type dep sort ind = let declare_individual_scheme_object name ?aux f = let f : individual_scheme_object_function = - fun _ ind -> f ind, Evd.empty_side_effects + fun _ ind -> f ind in declare_individual_scheme_object name ?aux f diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 98da61781e..7c702eab3a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -229,7 +229,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Evd.empty_side_effects) + (c, ctx)) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -248,17 +248,17 @@ let sym_scheme_kind = (**********************************************************************) let const_of_scheme kind env ind ctx = - let sym_scheme, eff = (find_scheme kind ind) in + let sym_scheme = match lookup_scheme kind ind with Some cst -> cst | None -> assert false in let sym, ctx = with_context_set ctx (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in - mkConstU sym, ctx, eff + mkConstU sym, ctx let build_sym_involutive_scheme env ind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in - let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in + let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in let inds = snd (mind_arity mip) in let indr = Sorts.relevance_of_sort_family inds in @@ -297,10 +297,11 @@ let build_sym_involutive_scheme env ind = mkRel 1|])), mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) - in (c, UState.of_context_set ctx), eff + in (c, UState.of_context_set ctx) let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" + ~deps:(fun ind -> [SchemeIndividualDep (ind, sym_scheme_kind)]) (fun _ ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) @@ -368,8 +369,8 @@ let build_l2r_rew_scheme dep env ind kind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in - let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in - let sym_involutive, ctx, eff' = const_of_scheme sym_involutive_scheme_kind env ind ctx in + let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in + let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env ind ctx in let eq,eqrefl,ctx = get_coq_eq ctx in let cstr n p = mkApp (mkConstructUi(indu,1), @@ -454,8 +455,7 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, UState.of_context_set ctx), - Evd.concat_side_effects eff' eff + in (c, UState.of_context_set ctx) (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -698,6 +698,10 @@ let build_r2l_rew_scheme dep env ind k = (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" + ~deps:(fun ind -> [ + SchemeIndividualDep (ind, sym_scheme_kind); + SchemeIndividualDep (ind, sym_involutive_scheme_kind); + ]) (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) @@ -708,7 +712,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -718,7 +722,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -728,7 +732,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -742,7 +746,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType)) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -752,7 +756,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType) (* End of rewriting schemes *) @@ -835,5 +839,4 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, - Evd.empty_side_effects) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index d1038f2655..6447708ace 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> - constr Evd.in_evar_universe_context * Evd.side_effects + constr Evd.in_evar_universe_context val build_r2l_forward_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Evd.side_effects + constr Evd.in_evar_universe_context val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 49645d82a4..e1d34af13e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -411,8 +411,7 @@ let find_elim hdcncl lft2rgt dep cls ot = match EConstr.kind sigma hdcncl with | Ind (ind,u) -> - let c, eff = find_scheme scheme_name ind in - Proofview.tclEFFECTS eff <*> + find_scheme scheme_name ind >>= fun c -> pf_constr_of_global (GlobRef.ConstRef c) | _ -> assert false end @@ -1001,14 +1000,13 @@ let ind_scheme_of_eq lbeq to_kind = let from_kind = inductive_sort_family mip in (* use ind rather than case by compatibility *) let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in - let c, eff = find_scheme kind (destIndRef lbeq.eq) in - GlobRef.ConstRef c, eff + find_scheme kind (destIndRef lbeq.eq) >>= fun c -> + Proofview.tclUNIT (GlobRef.ConstRef c) let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = build_coq_I () >>= fun i -> - let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in - Proofview.tclEFFECTS eff <*> + ind_scheme_of_eq lbeq to_kind >>= fun eq_elim -> pf_constr_of_global eq_elim >>= fun eq_elim -> Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) @@ -1045,7 +1043,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 = Clenvtac.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] + [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1347,23 +1345,23 @@ let inject_if_homogenous_dependent_pair ty = (* and compare the fst arguments of the dep pair *) (* Note: should work even if not an inductive type, but the table only *) (* knows inductive types *) - if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && + if not (Option.has_some (Ind_tables.lookup_scheme (!eq_dec_scheme_kind_name()) ind) && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in - let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in + find_scheme (!eq_dec_scheme_kind_name()) ind >>= fun c -> (* cut with the good equality and prove the requested goal *) tclTHENLIST - [Proofview.tclEFFECTS eff; + [ intro; onLastHyp (fun hyp -> Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr - (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))) + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> Proofview.tclUNIT () @@ -1408,7 +1406,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; - Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]) + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e422366ed6..9164a4ff26 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -32,9 +32,9 @@ type internal_flag = | UserIndividualRequest (* user action, a message is displayed *) type mutual_scheme_object_function = - internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context type 'a scheme_kind = string @@ -46,9 +46,13 @@ let pr_scheme_kind = Pp.str type individual type mutual +type scheme_dependency = +| SchemeMutualDep of MutInd.t * mutual scheme_kind +| SchemeIndividualDep of inductive * individual scheme_kind + type scheme_object_function = - | MutualSchemeFunction of mutual_scheme_object_function - | IndividualSchemeFunction of individual_scheme_object_function + | MutualSchemeFunction of mutual_scheme_object_function * (MutInd.t -> scheme_dependency list) option + | IndividualSchemeFunction of individual_scheme_object_function * (inductive -> scheme_dependency list) option let scheme_object_table = (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) @@ -68,11 +72,11 @@ let declare_scheme_object s aux f = Hashtbl.add scheme_object_table key (s,f); key -let declare_mutual_scheme_object s ?(aux="") f = - declare_scheme_object s aux (MutualSchemeFunction f) +let declare_mutual_scheme_object s ?deps ?(aux="") f = + declare_scheme_object s aux (MutualSchemeFunction (f, deps)) -let declare_individual_scheme_object s ?(aux="") f = - declare_scheme_object s aux (IndividualSchemeFunction f) +let declare_individual_scheme_object s ?deps ?(aux="") f = + declare_scheme_object s aux (IndividualSchemeFunction (f, deps)) (**********************************************************************) (* Defining/retrieving schemes *) @@ -89,6 +93,11 @@ let compute_name internal id = let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c -> CErrors.anomaly (Pp.str "scheme declaration not registered")) +let lookup_scheme kind ind = + try Some (DeclareScheme.lookup_scheme kind ind) with Not_found -> None + +let check_scheme kind ind = Option.has_some (lookup_scheme kind ind) + let define internal role id c poly univs = let id = compute_name internal id in let ctx = UState.minimize univs in @@ -96,8 +105,9 @@ let define internal role id c poly univs = let univs = UState.univ_entry ~poly ctx in !declare_definition_scheme ~internal ~univs ~role ~name:id c -let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = - let (c, ctx), eff = f mode ind in +(* Assumes that dependencies are already defined *) +let rec define_individual_scheme_base kind suff f mode idopt (mind,i as ind) eff = + let (c, ctx) = f mode ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id @@ -105,17 +115,21 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let role = Evd.Schema (ind, kind) in let internal = mode == InternalTacticRequest in let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in + let eff = Evd.concat_side_effects neff eff in DeclareScheme.declare_scheme kind [|ind,const|]; - const, Evd.concat_side_effects neff eff + const, eff -let define_individual_scheme kind mode names (mind,i as ind) = +and define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with - | _,MutualSchemeFunction f -> assert false - | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode names ind - -let define_mutual_scheme_base kind suff f mode names mind = - let (cl, ctx), eff = f mode mind in + | _,MutualSchemeFunction _ -> assert false + | s,IndividualSchemeFunction (f, deps) -> + let deps = match deps with None -> [] | Some deps -> deps ind in + let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in + define_individual_scheme_base kind s f mode names ind eff + +(* Assumes that dependencies are already defined *) +and define_mutual_scheme_base kind suff f mode names mind eff = + let (cl, ctx) = f mode mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names @@ -131,34 +145,49 @@ let define_mutual_scheme_base kind suff f mode names mind = DeclareScheme.declare_scheme kind schemes; consts, eff -let define_mutual_scheme kind mode names mind = +and define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false - | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f mode names mind - -let find_scheme_on_env_too kind ind = - let s = DeclareScheme.lookup_scheme kind ind in - s, Evd.empty_side_effects + | s,MutualSchemeFunction (f, deps) -> + let deps = match deps with None -> [] | Some deps -> deps mind in + let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in + define_mutual_scheme_base kind s f mode names mind eff + +and declare_scheme_dependence mode eff = function +| SchemeIndividualDep (ind, kind) -> + if check_scheme kind ind then eff + else + let _, eff' = define_individual_scheme kind mode None ind in + Evd.concat_side_effects eff' eff +| SchemeMutualDep (mind, kind) -> + if check_scheme kind (mind, 0) then eff + else + let _, eff' = define_mutual_scheme kind mode [] mind in + Evd.concat_side_effects eff' eff let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = - try find_scheme_on_env_too kind ind - with Not_found -> + let open Proofview.Notations in + match lookup_scheme kind ind with + | Some s -> + (* FIXME: we need to perform this call to reset the environment, since the + imperative scheme table is desynchronized from the monadic interface. *) + Proofview.tclEFFECTS Evd.empty_side_effects <*> + Proofview.tclUNIT s + | None -> match Hashtbl.find scheme_object_table kind with - | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode None ind - | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f mode [] mind in - ca.(i), eff + | s,IndividualSchemeFunction (f, deps) -> + let deps = match deps with None -> [] | Some deps -> deps ind in + let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in + let c, eff = define_individual_scheme_base kind s f mode None ind eff in + Proofview.tclEFFECTS eff <*> Proofview.tclUNIT c + | s,MutualSchemeFunction (f, deps) -> + let deps = match deps with None -> [] | Some deps -> deps mind in + let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in + let ca, eff = define_mutual_scheme_base kind s f mode [] mind eff in + Proofview.tclEFFECTS eff <*> Proofview.tclUNIT ca.(i) let define_individual_scheme kind mode names ind = ignore (define_individual_scheme kind mode names ind) let define_mutual_scheme kind mode names mind = ignore (define_mutual_scheme kind mode names mind) - -let check_scheme kind ind = - try let _ = find_scheme_on_env_too kind ind in true - with Not_found -> false - -let lookup_scheme = DeclareScheme.lookup_scheme diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 736de2af37..09fb051194 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -25,19 +25,27 @@ type internal_flag = | InternalTacticRequest | UserIndividualRequest +type scheme_dependency = +| SchemeMutualDep of MutInd.t * mutual scheme_kind +| SchemeIndividualDep of inductive * individual scheme_kind + type mutual_scheme_object_function = - internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context (** Main functions to register a scheme builder. Note these functions are not safe to be used by plugins as their effects won't be undone on backtracking *) -val declare_mutual_scheme_object : string -> ?aux:string -> +val declare_mutual_scheme_object : string -> + ?deps:(MutInd.t -> scheme_dependency list) -> + ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind -val declare_individual_scheme_object : string -> ?aux:string -> +val declare_individual_scheme_object : string -> + ?deps:(inductive -> scheme_dependency list) -> + ?aux:string -> individual_scheme_object_function -> individual scheme_kind @@ -51,12 +59,10 @@ val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) - (int * Id.t) list -> MutInd.t -> unit (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects - -val check_scheme : 'a scheme_kind -> inductive -> bool +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t Proofview.tactic -(** Like [find_scheme] but fails when the scheme is not already in the cache *) -val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t +(** Like [find_scheme] but does not generate a constant on the fly *) +val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t option val pr_scheme_kind : 'a scheme_kind -> Pp.t diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 8f6844079b..07f9def2c8 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -368,6 +368,9 @@ module New = struct Proofview.Unsafe.tclNEWGOALS tl <*> Proofview.tclUNIT ans + let tclTHENSLASTn t1 repeat l = + tclTHENS3PARTS t1 [||] repeat l + let tclTHENLASTn t1 l = tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 9ec558f1ad..01565169ca 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -180,6 +180,7 @@ module New : sig middle. Raises an error if the number of resulting subgoals is strictly less than [n+m] *) val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic + val tclTHENSLASTn : unit tactic -> unit tactic -> unit tactic array -> unit tactic val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0df4f5b207..e4809332c5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1368,7 +1368,7 @@ let clenv_refine_in 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 = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in + let exact_tac = Refiner.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 @@ -1670,7 +1670,7 @@ let descend_in_conjunctions avoid tac (err, info) c = | Some (p,pt) -> Tacticals.New.tclTHENS (assert_before_gen false (NamingAvoid avoid) pt) - [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p)); + [refiner ~check:true EConstr.Unsafe.(to_constr p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] end))) |