diff options
| -rw-r--r-- | tactics/elim.ml | 19 | ||||
| -rw-r--r-- | tactics/elim.mli | 3 | ||||
| -rw-r--r-- | tactics/inv.ml | 269 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 57 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 20 |
5 files changed, 240 insertions, 128 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 714f56e78..4cb44c31e 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -37,13 +37,20 @@ let introElimAssumsThen tac ba = let introCaseAssumsThen tac ba = let case_thin_sign = - List.flatten - (List.map - (function b -> if b then [false;true] else [false]) - ba.branchsign) + List.flatten + (List.map (function b -> if b then [false;true] else [false]) + ba.branchsign) in - let introCaseAssums = intros_clearing case_thin_sign in - (tclTHEN introCaseAssums (case_on_ba tac ba)) + let n1 = List.length case_thin_sign in + let n2 = List.length ba.branchnames in + let (l1,l2),l3 = + if n1 < n2 then list_chop n1 ba.branchnames, [] + else + (ba.branchnames, []), + if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in + let introCaseAssums = tclTHEN (intros_pattern None l1) (intros_clearing l3) + in + (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate diff --git a/tactics/elim.mli b/tactics/elim.mli index b0fb3981f..0fb104310 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -22,7 +22,8 @@ val introElimAssumsThen : (branch_assumptions -> tactic) -> branch_args -> tactic val introCaseAssumsThen : - (branch_assumptions -> tactic) -> branch_args -> tactic + (Tacexpr.intro_pattern_expr list -> branch_assumptions -> tactic) -> + branch_args -> tactic val general_decompose : (identifier * constr -> bool) -> constr -> tactic val decompose_nonrec : constr -> tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index f76729fa2..9f2691b06 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -26,7 +26,6 @@ open Proof_type open Evar_refiner open Clenv open Tactics -open Wcclausenv open Tacticals open Tactics open Elim @@ -35,6 +34,7 @@ open Typing open Pattern open Matching open Rawterm +open Tacexpr let collect_meta_variables c = let rec collrec acc c = match kind_of_term c with @@ -90,8 +90,7 @@ let compute_eqn env sigma n i ai = (ai,get_type_of env sigma ai), (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) -let make_inv_predicate env sigma ind id status concl = - let indf,realargs = dest_ind_type ind in +let make_inv_predicate env sigma indf realargs id status concl = let nrealargs = List.length realargs in let (hyps,concl) = match status with @@ -195,7 +194,7 @@ let rec dependent_hyps id idlist sign = let rec dep_rec =function | [] -> [] | (id1,_,id1ty as d1)::l -> - if occur_var (Global.env()) id (body_of_type id1ty) + if occur_var (Global.env()) id id1ty then d1 :: dep_rec l else dep_rec l in @@ -209,12 +208,93 @@ let split_dep_and_nodep hyps gl = open Coqlib +(* Computation of dids is late; must have been done in rewrite_equations*) +(* Will keep generalizing and introducing back and forth... *) +(* Moreover, others hyps depending of dids should have been *) +(* generalized; in such a way that [dids] can endly be cleared *) +(* Consider for instance this case extracted from Well_Ordering.v + + A : Set + B : A ->Set + a0 : A + f : (B a0) ->WO + y : WO + H0 : (le_WO y (sup a0 f)) + ============================ + (Acc WO le_WO y) + + Inversion H0 gives + + A : Set + B : A ->Set + a0 : A + f : (B a0) ->WO + y : WO + H0 : (le_WO y (sup a0 f)) + a1 : A + f0 : (B a1) ->WO + v : (B a1) + H1 : (f0 v)=y + H3 : a1=a0 + f1 : (B a0) ->WO + v0 : (B a0) + H4 : (existS A [a:A](B a) ->WO a0 f1)=(existS A [a:A](B a) ->WO a0 f) + ============================ + (Acc WO le_WO (f1 v0)) + +while, ideally, we would have expected + + A : Set + B : A ->Set + a0 : A + f0 : (B a0)->WO + v : (B a0) + ============================ + (Acc WO le_WO (f0 v)) + +obtained from destruction with equalities + + A : Set + B : A ->Set + a0 : A + f : (B a0) ->WO + y : WO + H0 : (le_WO y (sup a0 f)) + a1 : A + f0 : (B a1)->WO + v : (B a1) + H1 : (f0 v)=y + H2 : (sup a1 f0)=(sup a0 f) + ============================ + (Acc WO le_WO (f0 v)) + +by clearing initial hypothesis H0 and its dependency y, clearing H1 +(in fact H1 can be avoided using the same trick as for newdestruct), +decomposing H2 to get a1=a0 and (a1,f0)=(a0,f), replacing a1 by a0 +everywhere and removing a1 and a1=a0 (in fact it would have been more +regular to replace a0 by a1, avoiding f1 and v0 cannot replace f0 and v), +finally removing H4 (here because f is not used, more generally after using +eq_dep and replacing f by f0) [and finally rename a0, f0 into a,f]. +Summary: nine useless hypotheses! +Nota: with Inversion_clear, only four useless hypotheses +*) + let generalizeRewriteIntros tac depids id gls = let dids = dependent_hyps id depids (pf_env gls) in (tclTHENSEQ - [bring_hyps dids; tac; intros_replacing (ids_of_named_context dids)]) + [bring_hyps dids; tac; + (* may actually fail to replace if dependent in a previous eq *) + intros_replacing (ids_of_named_context dids)]) gls +let rec tclMAP_i n tacfun = function + | [] -> + if n>0 then tclDO n (tacfun None) + else tclIDTAC + | a::l -> + if n=0 then error "Too much names" + else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) + (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input It simplifies the clause (an equality) to use it as a rewrite rule and then @@ -223,41 +303,38 @@ let generalizeRewriteIntros tac depids id gls = If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) -let projectAndApply thin id depids gls = +let projectAndApply thin id eqname names depids gls = let env = pf_env gls in - let subst_hyp_LR id = tclTRY(hypSubst_LR id None) in - let subst_hyp_RL id = tclTRY(hypSubst_RL id None) in - let subst_hyp gls = - let orient_rule id = - let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in - match (kind_of_term t1, kind_of_term t2) with - | Var id1, _ -> - generalizeRewriteIntros (subst_hyp_LR id) depids id1 - | _, Var id2 -> - generalizeRewriteIntros (subst_hyp_RL id) depids id2 - | _ -> subst_hyp_RL id - in - onLastHyp orient_rule gls + let clearer = if thin then clear else fun _ -> tclIDTAC in + let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id None)) (clearer [id]) in + let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id None)) (clearer [id]) in + let substHypIfVariable tac id gls = + eqname := Some id; (* remember where to re-intro hyps later *) + let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in + match (kind_of_term t1, kind_of_term t2) with + | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls + | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls + | _ -> + tac id gls + in + let deq_trailer id neqns = + tclTHENSEQ + [(if names <> [] then clear [id] else tclIDTAC); + (tclMAP_i neqns (fun idopt -> + tclTHEN + (intro_move idopt None) + (* try again to substitute and if still not a variable after *) + (* decomposition, arbitraryly try to rewrite RL !? *) + (onLastHyp (substHypIfVariable subst_hyp_RL))) + names); + (if names = [] then clear [id] else tclIDTAC)] in - let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in - match (thin, kind_of_term t1, kind_of_term t2) with - | (true, Var id1, _) -> - generalizeRewriteIntros - (tclTHEN (subst_hyp_LR id) (clear [id])) depids id1 gls - | (false, Var id1, _) -> - generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls - | (true, _ , Var id2) -> - generalizeRewriteIntros - (tclTHEN (subst_hyp_RL id) (clear [id])) depids id2 gls - | (false, _ , Var id2) -> - generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls - | _ -> - let trailer = - if thin then onLastHyp (fun id -> clear [id]) else tclIDTAC in - let deq_trailer neqns = - tclDO neqns - (tclTHENSEQ [intro; tclTRY subst_hyp; trailer]) in - (tclTHEN (dEqThen deq_trailer (Some (NamedHyp id))) (clear [id])) gls + substHypIfVariable + (* If no immediate variable in the equation, try to decompose it *) + (* and apply a trailer which again try to substitute *) + (fun id -> dEqThen (deq_trailer id) (Some (NamedHyp id))) + id + gls (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer soi-meme (proposition de Valerie). *) @@ -273,7 +350,9 @@ let rewrite_equations_gene othin neqns ba gl = (tclTHEN intro (onLastHyp (fun id -> - tclTRY (projectAndApply thin id depids)))); + tclTRY + (projectAndApply thin id (ref None) + [] depids)))); onHyps (compose List.rev (afterHyp last)) bring_hyps; onHyps (afterHyp last) (compose clear ids_of_named_context)]) @@ -297,19 +376,46 @@ let rewrite_equations_gene othin neqns ba gl = None: the equations are introduced, but not rewritten Some thin: the equations are rewritten, and cleared if thin is true *) -let rewrite_equations othin neqns ba gl = +let rec get_names allow_conj = function + | IntroWildcard -> + error "Discarding pattern not allowed for inversion equations" + | IntroOrAndPattern [l] -> + if allow_conj then + if l = [] then (None,[]) else + let l = List.map (fun id -> out_some (fst (get_names false id))) l in + (Some (List.hd l), l) + else + error "Nested conjunctive patterns not allowed for inversion equations" + | IntroOrAndPattern l -> + error "Disjunctive patterns not allowed for inversion equations" + | IntroIdentifier id -> + (Some id,[id]) + +let extract_eqn_names = function + | None -> None,[] + | Some x -> x + +let rewrite_equations othin neqns names ba gl = + let names = List.map (get_names true) names in let (depids,nodepids) = split_dep_and_nodep ba.assums gl in let rewrite_eqns = + let first_eq = ref None in + let update id = if !first_eq = None then first_eq := Some id in match othin with | Some thin -> tclTHENSEQ [onHyps (compose List.rev (nLastHyps neqns)) bring_hyps; onHyps (nLastHyps neqns) (compose clear ids_of_named_context); - tclDO neqns - (tclTHEN intro - (onLastHyp - (fun id -> tclTRY (projectAndApply thin id depids)))); - tclDO (List.length nodepids) intro; + tclMAP_i neqns (fun o -> + let idopt,names = extract_eqn_names o in + (tclTHEN + (intro_move idopt None) + (onLastHyp (fun id -> + tclTRY (projectAndApply thin id first_eq names depids))))) + names; + tclMAP (fun (id,_,_) gl -> + intro_move None (if thin then None else !first_eq) gl) + nodepids; tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] | None -> tclIDTAC in @@ -320,17 +426,23 @@ let rewrite_equations othin neqns ba gl = rewrite_eqns]) gl -let rewrite_equations_tac (gene, othin) id neqns ba = +let interp_inversion_kind = function + | SimpleInversion -> None + | FullInversion -> Some false + | FullInversionClear -> Some true + +let rewrite_equations_tac (gene, othin) id neqns names ba = + let othin = interp_inversion_kind othin in let tac = if gene then rewrite_equations_gene othin neqns ba - else rewrite_equations othin neqns ba in + else rewrite_equations othin neqns names ba in if othin = Some true (* if Inversion_clear, clear the hypothesis *) then tclTHEN tac (tclTRY (clear [id])) else tac -let raw_inversion inv_kind indbinding id status gl = +let raw_inversion inv_kind indbinding id status names gl = let env = pf_env gl and sigma = project gl in let c = mkVar id in let (wc,kONT) = startWalk gl in @@ -340,13 +452,13 @@ let raw_inversion inv_kind indbinding id status gl = let newc = clenv_instance_template indclause' in let ccl = clenv_instance_template_type indclause' in check_no_metas indclause' ccl; - let (IndType (indf,realargs) as indt) = + let IndType (indf,realargs) = try find_rectype env sigma ccl with Not_found -> errorlabstrm "raw_inversion" (str ("The type of "^(string_of_id id)^" is not inductive")) in let (elim_predicate,neqns) = - make_inv_predicate env sigma indt id status (pf_concl gl) in + make_inv_predicate env sigma indf realargs id status (pf_concl gl) in let (cut_concl,case_tac) = if status <> NoDep & (dependent c (pf_concl gl)) then Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), @@ -357,15 +469,14 @@ let raw_inversion inv_kind indbinding id status gl = in (tclTHENS (true_cut None cut_concl) - [case_tac (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) - (Some elim_predicate) ([],[]) newc; + [case_tac names + (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) + (Some elim_predicate) ([],[]) newc; onLastHyp (fun id -> (tclTHEN - (applyUsing - (applist(mkVar id, - list_tabulate - (fun _ -> mkMeta(Clenv.new_meta())) neqns))) + (apply_term (mkVar id) + (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns)) reflexivity))]) gl @@ -399,44 +510,34 @@ let wrap_inv_error id = function | e -> raise e (* The most general inversion tactic *) -let inversion inv_kind status id gls = - try (raw_inversion inv_kind [] id status) gls +let inversion inv_kind status names id gls = + try (raw_inversion inv_kind [] id status names) gls with e -> wrap_inv_error id e (* Specializing it... *) -let inv_gen gene thin status = try_intros_until (inversion (gene,thin) status) +let inv_gen gene thin status names = + try_intros_until (inversion (gene,thin) status names) open Tacexpr -(* -let hinv_kind = Quoted_string "HalfInversion" -let inv_kind = Quoted_string "Inversion" -let invclr_kind = Quoted_string "InversionClear" - -let com_of_id id = - if id = hinv_kind then None - else if id = inv_kind then Some false - else Some true -*) - -let inv k id = inv_gen false k NoDep id +let inv k = inv_gen false k NoDep -let half_inv_tac id = inv None (NamedHyp id) -let inv_tac id = inv (Some false) (NamedHyp id) -let inv_clear_tac id = inv (Some true) (NamedHyp id) +let half_inv_tac id = inv SimpleInversion [] (NamedHyp id) +let inv_tac id = inv FullInversion [] (NamedHyp id) +let inv_clear_tac id = inv FullInversionClear [] (NamedHyp id) -let dinv k c id = inv_gen false k (Dep c) id +let dinv k c = inv_gen false k (Dep c) -let half_dinv_tac id = dinv None None (NamedHyp id) -let dinv_tac id = dinv (Some false) None (NamedHyp id) -let dinv_clear_tac id = dinv (Some true) None (NamedHyp id) +let half_dinv_tac id = dinv SimpleInversion None [] (NamedHyp id) +let dinv_tac id = dinv FullInversion None [] (NamedHyp id) +let dinv_clear_tac id = dinv FullInversionClear None [] (NamedHyp id) (* InvIn will bring the specified clauses into the conclusion, and then * perform inversion on the named hypothesis. After, it will intro them * back to their places in the hyp-list. *) -let invIn com id ids gls = +let invIn k names ids id gls = let hyps = List.map (pf_get_hyp gls) ids in let nb_prod_init = nb_prod (pf_concl gls) in let intros_replace_ids gls = @@ -450,8 +551,14 @@ let invIn com id ids gls = in try (tclTHENSEQ - [bring_hyps hyps; inversion (false, com) NoDep id; intros_replace_ids]) + [bring_hyps hyps; + inversion (false,k) NoDep names id; + intros_replace_ids]) gls with e -> wrap_inv_error id e -let invIn_gen com id idl = try_intros_until (fun id -> invIn com id idl) id +let invIn_gen k names idl = try_intros_until (invIn k names idl) + +let inv_clause k names = function + | [] -> inv k names + | idl -> invIn_gen k names idl diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b5fc4e253..09964a331 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -25,7 +25,7 @@ open Clenv open Pattern open Matching open Evar_refiner -open Wcclausenv +open Tacexpr (******************************************) (* Basic Tacticals *) @@ -239,25 +239,28 @@ type branch_args = { branchnum : int; (* the branch number *) pred : constr; (* the predicate we used *) nassums : int; (* the number of assumptions to be introduced *) - branchsign : bool list} (* the signature of the branch. + branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) + branchnames : intro_pattern_expr list} type branch_assumptions = { ba : branch_args; (* the branch args *) - assums : named_context; (* the list of assumptions introduced *) - cargs : identifier list; (* the constructor arguments *) - constargs : identifier list; (* the CONSTANT constructor arguments *) - recargs : identifier list; (* the RECURSIVE constructor arguments *) - indargs : identifier list} (* the inductive arguments *) + assums : named_context} (* the list of assumptions introduced *) + +let compute_induction_names n names = + let names = if names = [] then Array.make n [] else Array.of_list names in + if Array.length names <> n then + errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names"); + names let compute_construtor_signatures isrec (_,k as ity) = let rec analrec c recargs = match kind_of_term c, recargs with | Prod (_,_,c), recarg::rest -> - (match dest_recarg recarg with - | Norec -> false :: (analrec c rest) - | Imbr _ -> false :: (analrec c rest) - | Mrec j -> (isrec & j=k) :: (analrec c rest)) + let b = match dest_recarg recarg with + | Norec | Imbr _ -> false + | Mrec j -> isrec & j=k + in b :: (analrec c rest) | LetIn (_,_,_,c), rest -> false :: (analrec c rest) | _, [] -> [] | _ -> anomaly "compute_construtor_signatures" @@ -269,9 +272,6 @@ let compute_construtor_signatures isrec (_,k as ity) = let lrecargs = dest_subterms mip.mind_recargs in array_map2 analrec lc lrecargs -let case_sign = compute_construtor_signatures false -let elim_sign = compute_construtor_signatures true - let elimination_sort_of_goal gl = match kind_of_term (hnf_type_of gl (pf_concl gl)) with | Sort s -> @@ -299,7 +299,7 @@ let last_arg c = match kind_of_term c with | _ -> anomaly "last_arg" let general_elim_then_using - elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl = + elim isrec allnames tac predicate (indbindings,elimbindings) c gl = let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in (* applying elimination_scheme just a little modified *) let (wc,kONT) = startWalk gl in @@ -326,10 +326,12 @@ let general_elim_then_using in let elimclause' = clenv_fchain indmv elimclause indclause' in let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in - let branchsigns = elim_sign_fun ity in + let branchsigns = compute_construtor_signatures isrec ity in + let brnames = compute_induction_names (Array.length branchsigns) allnames in let after_tac ce i gl = let (hd,largs) = decompose_app (clenv_template_type ce).rebus in let ba = { branchsign = branchsigns.(i); + branchnames = brnames.(i); nassums = List.fold_left (fun acc b -> if b then acc+2 else acc+1) @@ -355,29 +357,30 @@ let elimination_then_using tac predicate (indbindings,elimbindings) c gl = let elim = Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in general_elim_then_using - elim elim_sign tac predicate (indbindings,elimbindings) c gl + elim true [] tac predicate (indbindings,elimbindings) c gl let elimination_then tac = elimination_then_using tac None let simple_elimination_then tac = elimination_then tac ([],[]) -let case_then_using tac predicate (indbindings,elimbindings) c gl = +let case_then_using allnames tac predicate (indbindings,elimbindings) c gl = (* finding the case combinator *) let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let sigma = project gl in let sort = elimination_sort_of_goal gl in let elim = Indrec.make_case_dep (pf_env gl) sigma ity sort in general_elim_then_using - elim case_sign tac predicate (indbindings,elimbindings) c gl + elim false allnames tac predicate (indbindings,elimbindings) c gl -let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl = +let case_nodep_then_using allnames tac predicate (indbindings,elimbindings) + c gl = (* finding the case combinator *) let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let sigma = project gl in let sort = elimination_sort_of_goal gl in let elim = Indrec.make_case_nodep (pf_env gl) sigma ity sort in general_elim_then_using - elim case_sign tac predicate (indbindings,elimbindings) c gl + elim false allnames tac predicate (indbindings,elimbindings) c gl let make_elim_branch_assumptions ba gl = @@ -385,11 +388,7 @@ let make_elim_branch_assumptions ba gl = match lb,lc with | ([], _) -> { ba = ba; - assums = assums; - cargs = cargs; - constargs = constargs; - recargs = recargs; - indargs = indargs} + assums = assums} | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) -> makerec (recarg::indarg::assums, idrec::cargs, @@ -415,11 +414,7 @@ let make_case_branch_assumptions ba gl = match p_0,p_1 with | ([], _) -> { ba = ba; - assums = assums; - cargs = cargs; - constargs = constargs; - recargs = recargs; - indargs = []} + assums = assums} | ((true::tl), ((idrec,_,_ as recarg)::idtl)) -> makerec (recarg::assums, idrec::cargs, diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4a1e03475..843a706b4 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -18,6 +18,7 @@ open Clenv open Reduction open Pattern open Wcclausenv +open Tacexpr (*i*) (* Tacticals i.e. functions from tactics to tactics. *) @@ -112,22 +113,23 @@ type branch_args = { branchnum : int; (* the branch number *) pred : constr; (* the predicate we used *) nassums : int; (* the number of assumptions to be introduced *) - branchsign : bool list } (* the signature of the branch. + branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) + branchnames : intro_pattern_expr list} type branch_assumptions = { ba : branch_args; (* the branch args *) - assums : named_context; (* the list of assumptions introduced *) - cargs : identifier list; (* the constructor arguments *) - constargs : identifier list; (* the CONSTANT constructor arguments *) - recargs : identifier list; (* the RECURSIVE constructor arguments *) - indargs : identifier list} (* the inductive arguments *) + assums : named_context} (* the list of assumptions introduced *) + +(* Useful for "as intro_pattern" modifier *) +val compute_induction_names : + int -> case_intro_pattern_expr -> intro_pattern_expr list array val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : identifier -> goal sigma -> sorts_family val general_elim_then_using : - constr -> (inductive -> bool list array) -> + constr -> (* isrec: *) bool -> case_intro_pattern_expr -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> constr -> tactic @@ -140,11 +142,11 @@ val elimination_then : (arg_bindings * arg_bindings) -> constr -> tactic val case_then_using : - (branch_args -> tactic) -> + case_intro_pattern_expr -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> constr -> tactic val case_nodep_then_using : - (branch_args -> tactic) -> + case_intro_pattern_expr -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> constr -> tactic val simple_elimination_then : |