(* A proof by pointing algorithm. *) open Util;; open Names;; open Term;; open Tactics;; open Tacticals;; open Hipattern;; open Pattern;; open Matching;; open Reduction;; open Rawterm;; open Environ;; open Proof_trees;; open Proof_type;; open Tacmach;; open Tacexpr;; open Typing;; open Pp;; open Libnames;; open Genarg;; open Topconstr;; open Termops;; let zz = Util.dummy_loc;; let hyp_radix = id_of_string "H";; let next_global_ident = next_global_ident_away true (* get_hyp_by_name : goal sigma -> string -> constr, looks up for an hypothesis (or a global constant), from its name *) let get_hyp_by_name g name = let evd = project g in let env = pf_env g in try (let judgment = Pretyping.understand_judgment evd env (RVar(zz, name)) in ("hyp",judgment.uj_type)) (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up... Loïc *) with _ -> (let c = Nametab.global (Ident (zz,name)) in ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c))) ;; type pbp_atom = | PbpTryAssumption of identifier option | PbpTryClear of identifier list | PbpGeneralize of identifier * identifier list | PbpLApply of identifier (* = CutAndApply *) | PbpIntros of intro_pattern_expr list | PbpSplit (* Existential *) | PbpExists of identifier (* Or *) | PbpLeft | PbpRight (* Head *) | PbpApply of identifier | PbpElim of identifier * identifier list;; (* Invariant: In PbpThens ([a1;...;an],[t1;...;tp]), all tactics [a1]..[an-1] are atomic (or try of an atomic) tactic and produce exactly one goal, and [an] produces exactly p subgoals In [PbpThen [a1;..an]], all tactics are (try of) atomic tactics and produces exactly one subgoal, except the last one which may complete the goal Convention: [PbpThen []] is Idtac and [PbpThen t] is a coercion from atomic to composed tactic *) type pbp_sequence = | PbpThens of pbp_atom list * pbp_sequence list | PbpThen of pbp_atom list (* This flattens sequences of tactics producing just one subgoal *) let chain_tactics tl1 = function | PbpThens (tl2, tl3) -> PbpThens (tl1@tl2, tl3) | PbpThen tl2 -> PbpThen (tl1@tl2) type pbp_rule = (identifier list * identifier list * bool * identifier option * (types, constr) kind_of_term * int list * (identifier list -> identifier list -> bool -> identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) -> pbp_sequence option;; let make_named_intro id = PbpIntros [IntroIdentifier id];; let make_clears str_list = PbpThen [PbpTryClear str_list] let add_clear_names_if_necessary tactic clear_names = match clear_names with [] -> tactic | l -> chain_tactics [PbpTryClear l] tactic;; let make_final_cmd f optname clear_names constr path = add_clear_names_if_necessary (f optname constr path) clear_names;; let (rem_cast:pbp_rule) = function (a,c,cf,o, Cast(f,_), p, func) -> Some(func a c cf o (kind_of_term f) p) | _ -> None;; let (forall_intro: pbp_rule) = function (avoid, clear_names, clear_flag, None, Prod(Name x, _, body), (2::path), f) -> let x' = next_global_ident x avoid in Some(chain_tactics [make_named_intro x'] (f (x'::avoid) clear_names clear_flag None (kind_of_term body) path)) | _ -> None;; let (imply_intro2: pbp_rule) = function avoid, clear_names, clear_flag, None, Prod(Anonymous, _, body), 2::path, f -> let h' = next_global_ident hyp_radix avoid in Some(chain_tactics [make_named_intro h'] (f (h'::avoid) clear_names clear_flag None (kind_of_term body) path)) | _ -> None;; (* let (imply_intro1: pbp_rule) = function avoid, clear_names, clear_flag, None, Prod(Anonymous, prem, body), 1::path, f -> let h' = next_global_ident hyp_radix avoid in let str_h' = h' in Some(chain_tactics [make_named_intro str_h'] (f (h'::avoid) clear_names clear_flag (Some str_h') (kind_of_term prem) path)) | _ -> None;; *) let make_var id = CRef (Ident(zz, id)) let make_app f l = CApp (zz,(None,f),List.map (fun x -> (x,None)) l) let make_pbp_pattern x = make_app (make_var (id_of_string "PBP_META")) [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))] let rec make_then = function | [] -> TacId "" | [t] -> t | t1::t2::l -> make_then (TacThen (t1,t2)::l) let make_pbp_atomic_tactic = function | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption)) | PbpTryAssumption (Some a) -> TacTry (TacAtom (zz, TacExact (make_var a))) | PbpExists x -> TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in TacAtom (zz, TacGeneralize [make_app (make_var h) l]) | PbpLeft -> TacAtom (zz, TacLeft NoBindings) | PbpRight -> TacAtom (zz, TacRight NoBindings) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) | PbpLApply h -> TacAtom (zz, TacLApply (make_var h)) | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings)) | PbpElim (hyp_name, names) -> let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in TacAtom (zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l))) | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));; let rec make_pbp_tactic = function | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl) | PbpThens (l,tl) -> TacThens (make_then (List.map make_pbp_atomic_tactic l), List.map make_pbp_tactic tl) let (forall_elim: pbp_rule) = function avoid, clear_names, clear_flag, Some h, Prod(Name x, _, body), 2::path, f -> let h' = next_global_ident hyp_radix avoid in let clear_names' = if clear_flag then h::clear_names else clear_names in Some (chain_tactics [PbpGeneralize (h,[x]); make_named_intro h'] (f (h'::avoid) clear_names' true (Some h') (kind_of_term body) path)) | _ -> None;; let (imply_elim1: pbp_rule) = function avoid, clear_names, clear_flag, Some h, Prod(Anonymous, prem, body), 1::path, f -> let clear_names' = if clear_flag then h::clear_names else clear_names in let h' = next_global_ident hyp_radix avoid in let str_h' = (string_of_id h') in Some(PbpThens ([PbpLApply h], [chain_tactics [make_named_intro h'] (make_clears (h::clear_names)); f avoid clear_names' false None (kind_of_term prem) path])) | _ -> None;; let (imply_elim2: pbp_rule) = function avoid, clear_names, clear_flag, Some h, Prod(Anonymous, prem, body), 2::path, f -> let clear_names' = if clear_flag then h::clear_names else clear_names in let h' = next_global_ident hyp_radix avoid in Some(PbpThens ([PbpLApply h], [chain_tactics [make_named_intro h'] (f (h'::avoid) clear_names' false (Some h') (kind_of_term body) path); make_clears clear_names])) | _ -> None;; let reference dir s = Coqlib.gen_reference "Pbp" ("Init"::dir) s let constant dir s = Coqlib.gen_constant "Pbp" ("Init"::dir) s let andconstr: unit -> constr = Coqlib.build_coq_and;; let prodconstr () = constant ["Datatypes"] "prod";; let exconstr = Coqlib.build_coq_ex;; let sigconstr () = constant ["Specif"] "sig";; let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ;; let orconstr = Coqlib.build_coq_or;; let sumboolconstr = Coqlib.build_coq_sumbool;; let sumconstr() = constant ["Datatypes"] "sum";; let notconstr = Coqlib.build_coq_not;; let notTconstr () = constant ["Logic_Type"] "notT";; let is_matching_local a b = is_matching (pattern_of_constr a) b;; let rec (or_and_tree_to_intro_pattern: identifier list -> constr -> int list -> intro_pattern_expr * identifier list * identifier *constr * int list * int * int) = fun avoid c path -> match kind_of_term c, path with | (App(oper, [|c1; c2|]), 2::a::path) when ((is_matching_local (andconstr()) oper) or (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) -> let id2 = next_global_ident hyp_radix avoid in let cont_expr = if a = 1 then c1 else c2 in let cont_patt, avoid_names, id, c, path, rank, total_branches = or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in let patt_list = if a = 1 then [cont_patt; IntroIdentifier id2] else [IntroIdentifier id2; cont_patt] in (IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank, total_branches) | (App(oper, [|c1; c2|]), 2::3::path) when ((is_matching_local (exconstr()) oper) or (is_matching_local (sigconstr()) oper)) -> (match (kind_of_term c2) with Lambda (Name x, _, body) -> let id1 = next_global_ident x avoid in let cont_patt, avoid_names, id, c, path, rank, total_branches = or_and_tree_to_intro_pattern (id1::avoid) body path in (IntroOrAndPattern[[IntroIdentifier id1; cont_patt]], avoid_names, id, c, path, rank, total_branches) | _ -> assert false) | (App(oper, [|c1; c2|]), 2::a::path) when ((is_matching_local (orconstr ()) oper) or (is_matching_local (sumboolconstr ()) oper) or (is_matching_local (sumconstr ()) oper)) & (a = 1 or a = 2) -> let id2 = next_global_ident hyp_radix avoid in let cont_expr = if a = 1 then c1 else c2 in let cont_patt, avoid_names, id, c, path, rank, total_branches = or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in let new_rank = if a = 1 then rank else rank+1 in let patt_list = if a = 1 then [[cont_patt];[IntroIdentifier id2]] else [[IntroIdentifier id2];[cont_patt]] in (IntroOrAndPattern patt_list, avoid_names, id, c, path, new_rank, total_branches+1) | (_, path) -> let id = next_global_ident hyp_radix avoid in (IntroIdentifier id, (id::avoid), id, c, path, 1, 1);; let auxiliary_goals clear_names clear_flag this_name n_aux others = let clear_cmd = make_clears (if clear_flag then (this_name ::clear_names) else clear_names) in let rec clear_list = function 0 -> others | n -> clear_cmd::(clear_list (n - 1)) in clear_list n_aux;; let (imply_intro3: pbp_rule) = function avoid, clear_names, clear_flag, None, Prod(Anonymous, prem, body), 1::path, f -> let intro_patt, avoid_names, id, c, p, rank, total_branches = or_and_tree_to_intro_pattern avoid prem path in if total_branches = 1 then Some(chain_tactics [PbpIntros [intro_patt]] (f avoid_names clear_names clear_flag (Some id) (kind_of_term c) path)) else Some (PbpThens ([PbpIntros [intro_patt]], auxiliary_goals clear_names clear_flag id (rank - 1) ((f avoid_names clear_names clear_flag (Some id) (kind_of_term c) path):: auxiliary_goals clear_names clear_flag id (total_branches - rank) []))) | _ -> None;; let (and_intro: pbp_rule) = function avoid, clear_names, clear_flag, None, App(and_oper, [|c1; c2|]), 2::a::path, f -> if ((is_matching_local (andconstr()) and_oper) or (is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then let cont_term = if a = 1 then c1 else c2 in let cont_cmd = f avoid clear_names false None (kind_of_term cont_term) path in let clear_cmd = make_clears clear_names in let cmds = (if a = 1 then [cont_cmd;clear_cmd] else [clear_cmd;cont_cmd]) in Some (PbpThens ([PbpSplit],cmds)) else None | _ -> None;; let exists_from_lambda avoid clear_names clear_flag c2 path f = match kind_of_term c2 with Lambda(Name x, _, body) -> Some (PbpThens ([PbpExists x], [f avoid clear_names false None (kind_of_term body) path])) | _ -> None;; let (ex_intro: pbp_rule) = function avoid, clear_names, clear_flag, None, App(oper, [| c1; c2|]), 2::3::path, f when (is_matching_local (exconstr ()) oper) or (is_matching_local (sigconstr ()) oper) -> exists_from_lambda avoid clear_names clear_flag c2 path f | _ -> None;; let (exT_intro : pbp_rule) = function avoid, clear_names, clear_flag, None, App(oper, [| c1; c2|]), 2::2::2::path, f when (is_matching_local (sigTconstr ()) oper) -> exists_from_lambda avoid clear_names clear_flag c2 path f | _ -> None;; let (or_intro: pbp_rule) = function avoid, clear_names, clear_flag, None, App(or_oper, [|c1; c2 |]), 2::a::path, f -> if ((is_matching_local (orconstr ()) or_oper) or (is_matching_local (sumboolconstr ()) or_oper) or (is_matching_local (sumconstr ()) or_oper)) & (a = 1 or a = 2) then let cont_term = if a = 1 then c1 else c2 in let fst_cmd = if a = 1 then PbpLeft else PbpRight in let cont_cmd = f avoid clear_names false None (kind_of_term cont_term) path in Some(chain_tactics [fst_cmd] cont_cmd) else None | _ -> None;; let dummy_id = id_of_string "Dummy";; let (not_intro: pbp_rule) = function avoid, clear_names, clear_flag, None, App(not_oper, [|c1|]), 2::1::path, f -> if(is_matching_local (notconstr ()) not_oper) or (is_matching_local (notTconstr ()) not_oper) then let h' = next_global_ident hyp_radix avoid in Some(chain_tactics [make_named_intro h'] (f (h'::avoid) clear_names false (Some h') (kind_of_term c1) path)) else None | _ -> None;; let elim_with_bindings hyp_name names = PbpElim (hyp_name, names);; (* This function is used to follow down a path, while staying on the spine of successive products (universal quantifications or implications). Arguments are the current observed constr object and the path that remains to be followed, and an integer indicating how many products have already been crossed. Result is: - a list of string indicating the names of universally quantified variables. - a list of integers indicating the positions of the successive universally quantified variables. - an integer indicating the number of non-dependent products. - the last constr object encountered during the walk down, and - the remaining path. For instance the following session should happen: let tt = raw_constr_of_com (Evd.mt_evd())(gLOB(initial_sign())) (parse_com "(P:nat->Prop)(x:nat)(P x)->(P x)") in down_prods (tt, [2;2;2], 0) ---> ["P","x"],[0;1], 1, <<(P x)>>, [] *) let rec down_prods: (types, constr) kind_of_term * (int list) * int -> identifier list * (int list) * int * (types, constr) kind_of_term * (int list) = function Prod(Name x, _, body), 2::path, k -> let res_sl, res_il, res_i, res_cstr, res_p = down_prods (kind_of_term body, path, k+1) in x::res_sl, (k::res_il), res_i, res_cstr, res_p | Prod(Anonymous, _, body), 2::path, k -> let res_sl, res_il, res_i, res_cstr, res_p = down_prods (kind_of_term body, path, k+1) in res_sl, res_il, res_i+1, res_cstr, res_p | cstr, path, _ -> [], [], 0, cstr, path;; exception Pbp_internal of int list;; (* This function should be usable to check that a type can be used by the Apply command. Basically, c is supposed to be the head of some type, where l gives the ranks of all universally quantified variables. It check that these universally quantified variables occur in the head. The knowledge I have on constr structures is incomplete. *) let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) = function c -> function l -> let rec delete n = function | [] -> [] | p::tl -> if n = p then tl else p::(delete n tl) in let rec check_rec l = function | App(f, array) -> Array.fold_left (fun l c -> check_rec l (kind_of_term c)) (check_rec l (kind_of_term f)) array | Const _ -> l | Ind _ -> l | Construct _ -> l | Var _ -> l | Rel p -> let result = delete p l in if result = [] then raise (Pbp_internal []) else result | _ -> raise (Pbp_internal l) in try (check_rec l c) = [] with Pbp_internal l -> l = [];; let (mk_db_indices: int list -> int -> int list) = function int_list -> function nprems -> let total = (List.length int_list) + nprems in let rec mk_db_aux = function [] -> [] | a::l -> (total - a)::(mk_db_aux l) in mk_db_aux int_list;; (* This proof-by-pointing rule is quite complicated, as it attempts to foresee usages of head tactics. A first operation is to follow the path as far as possible while staying on the spine of products (function down_prods) and then to check whether the next step will be an elim step. If the answer is true, then the built command takes advantage of the power of head tactics. *) let (head_tactic_patt: pbp_rule) = function avoid, clear_names, clear_flag, Some h, cstr, path, f -> (match down_prods (cstr, path, 0) with | (str_list, _, nprems, App(oper,[|c1; c2|]), b::a::path) when (((is_matching_local (exconstr ()) oper) (* or (is_matching_local (sigconstr ()) oper) *)) && a = 3) -> (match (kind_of_term c2) with Lambda(Name x, _,body) -> Some(PbpThens ([elim_with_bindings h str_list], let x' = next_global_ident x avoid in let cont_body = Prod(Name x', c1, mkProd(Anonymous, body, mkVar(dummy_id))) in let cont_tac = f avoid (h::clear_names) false None cont_body (2::1::path) in cont_tac::(auxiliary_goals clear_names clear_flag h nprems []))) | _ -> None) | (str_list, _, nprems, App(oper,[|c1|]), 2::1::path) when (is_matching_local (notconstr ()) oper) or (is_matching_local (notTconstr ()) oper) -> Some(chain_tactics [elim_with_bindings h str_list] (f avoid clear_names false None (kind_of_term c1) path)) | (str_list, _, nprems, App(oper, [|c1; c2|]), 2::a::path) when ((is_matching_local (andconstr()) oper) or (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) -> let h1 = next_global_ident hyp_radix avoid in let h2 = next_global_ident hyp_radix (h1::avoid) in Some(PbpThens ([elim_with_bindings h str_list], let cont_body = if a = 1 then c1 else c2 in let cont_tac = f (h2::h1::avoid) (h::clear_names) false (Some (if 1 = a then h1 else h2)) (kind_of_term cont_body) path in (chain_tactics [make_named_intro h1; make_named_intro h2] cont_tac):: (auxiliary_goals clear_names clear_flag h nprems []))) | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path) when ((is_matching_local (sigTconstr()) oper)) & a = 2 -> (match (kind_of_term c2),path with Lambda(Name x, _,body), (2::path) -> Some(PbpThens ([elim_with_bindings h str_list], let x' = next_global_ident x avoid in let cont_body = Prod(Name x', c1, mkProd(Anonymous, body, mkVar(dummy_id))) in let cont_tac = f avoid (h::clear_names) false None cont_body (2::1::path) in cont_tac::(auxiliary_goals clear_names clear_flag h nprems []))) | _ -> None) | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path) when ((is_matching_local (orconstr ()) oper) or (is_matching_local (sumboolconstr ()) oper) or (is_matching_local (sumconstr ()) oper)) & (a = 1 or a = 2) -> Some(PbpThens ([elim_with_bindings h str_list], let cont_body = if a = 1 then c1 else c2 in (* h' is the name for the new intro *) let h' = next_global_ident hyp_radix avoid in let cont_tac = chain_tactics [make_named_intro h'] (f (* h' should not be used again *) (h'::avoid) (* the disjunct itself can be discarded *) (h::clear_names) false (Some h') (kind_of_term cont_body) path) in let snd_tac = chain_tactics [make_named_intro h'] (make_clears (h::clear_names)) in let tacs1 = if a = 1 then [cont_tac; snd_tac] else [snd_tac; cont_tac] in tacs1@(auxiliary_goals (h::clear_names) false dummy_id nprems []))) | (str_list, int_list, nprems, c, []) when (check_apply c (mk_db_indices int_list nprems)) & (match c with Prod(_,_,_) -> false | _ -> true) & (List.length int_list) + nprems > 0 -> Some(add_clear_names_if_necessary (PbpThen [PbpApply h]) clear_names) | _ -> None) | _ -> None;; let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2; forall_elim; imply_intro3; imply_elim1; imply_elim2; and_intro; or_intro; not_intro; ex_intro; exT_intro];; let try_trace = ref true;; let traced_try (f1:tactic) g = try (try_trace := true; tclPROGRESS f1 g) with e when Logic.catchable_exception e -> (try_trace := false; tclIDTAC g);; let traced_try_entry = function [Tacexp t] -> traced_try (Tacinterp.interp t) | _ -> failwith "traced_try_entry received wrong arguments";; (* When the recursive descent along the path is over, one includes the command requested by the point-and-shoot strategy. Default is Try Assumption--Try Exact. *) let default_ast optname constr path = PbpThen [PbpTryAssumption optname] (* This is the main proof by pointing function. *) (* avoid: les noms a ne pas utiliser *) (* final_cmd: la fonction appelee par defaut *) (* opt_name: eventuellement le nom de l'hypothese sur laquelle on agit *) let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path = let rec try_all_rules rl = match rl with f::tl -> (match f (avoid, clear_names, clear_flag, opt_name, constr, path, pbpt final_cmd) with Some(ast) -> ast | None -> try_all_rules tl) | [] -> make_final_cmd final_cmd opt_name clear_names constr path in try_all_rules (!pbp_rules);; (* these are the optimisation functions. *) (* This function takes care of flattening successive then commands. *) (* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy that t is some [PbpAtom t] *) (* This optimization function takes care of compacting successive Intro commands together. *) let rec group_intros names = function [] -> (match names with [] -> [] | l -> [PbpIntros l]) | (PbpIntros ids)::others -> group_intros (names@ids) others | t1::others -> (match names with [] -> t1::(group_intros [] others) | l -> (PbpIntros l)::t1::(group_intros [] others)) let rec optim2 = function | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2) | PbpThen tl -> PbpThen (group_intros [] tl) let rec cleanup_clears str_list = function [] -> [] | x::tail -> if List.mem x str_list then cleanup_clears str_list tail else x::(cleanup_clears str_list tail);; (* This function takes care of compacting instanciations of universal quantifications. *) let rec optim3_aux str_list = function (PbpGeneralize (h,l1)):: (PbpIntros [IntroIdentifier s])::(PbpGeneralize (h',l2))::others when s=h' -> optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others) | (PbpTryClear names)::other -> (match cleanup_clears str_list names with [] -> other | l -> (PbpTryClear l)::other) | a::l -> a::(optim3_aux str_list l) | [] -> [];; let rec optim3 str_list = function PbpThens (tl1, tl2) -> PbpThens (optim3_aux str_list tl1, List.map (optim3 str_list) tl2) | PbpThen tl -> PbpThen (optim3_aux str_list tl) let optim x = make_pbp_tactic (optim3 [] (optim2 x));; (* TODO add_tactic "Traced_Try" traced_try_entry;; *) let rec tactic_args_to_ints = function [] -> [] | (Integer n)::l -> n::(tactic_args_to_ints l) | _ -> failwith "expecting only numbers";; (* let pbp_tac display_function = function (Identifier a)::l -> (function g -> let str = (string_of_id a) in let (ou,tstr) = (get_hyp_by_name g str) in let exp_ast = pbpt default_ast (match ou with "hyp" ->(pf_ids_of_hyps g) |_ -> (a::(pf_ids_of_hyps g))) [] false (Some str) (kind_of_term tstr) (tactic_args_to_ints l) in (display_function (optim exp_ast); tclIDTAC g)) | ((Integer n)::_) as l -> (function g -> let exp_ast = (pbpt default_ast (pf_ids_of_hyps g) [] false None (kind_of_term (pf_concl g)) (tactic_args_to_ints l)) in (display_function (optim exp_ast); tclIDTAC g)) | [] -> (function g -> (display_function (default_ast None (pf_concl g) []); tclIDTAC g)) | _ -> failwith "expecting other arguments";; *) let pbp_tac display_function idopt nl = match idopt with | Some str -> (function g -> let (ou,tstr) = (get_hyp_by_name g str) in let exp_ast = pbpt default_ast (match ou with "hyp" ->(pf_ids_of_hyps g) |_ -> (str::(pf_ids_of_hyps g))) [] false (Some str) (kind_of_term tstr) nl in (display_function (optim exp_ast); tclIDTAC g)) | None -> if nl <> [] then (function g -> let exp_ast = (pbpt default_ast (pf_ids_of_hyps g) [] false None (kind_of_term (pf_concl g)) nl) in (display_function (optim exp_ast); tclIDTAC g)) else (function g -> (display_function (make_pbp_tactic (default_ast None (pf_concl g) [])); tclIDTAC g));;