diff options
Diffstat (limited to 'tactics/inv.ml')
-rw-r--r-- | tactics/inv.ml | 479 |
1 files changed, 236 insertions, 243 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 73edaf86..5502356f 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,63 +1,40 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util open Names open Nameops open Term +open Vars +open Context open Termops open Namegen -open Global -open Sign open Environ open Inductiveops open Printer -open Reductionops open Retyping -open Tacmach -open Proof_type -open Evar_refiner -open Clenv -open Tactics -open Tacticals +open Tacmach.New +open Tacticals.New open Tactics open Elim open Equality -open Typing -open Pattern -open Matching -open Glob_term -open Genarg +open Misctypes open Tacexpr +open Proofview.Notations -let collect_meta_variables c = - let rec collrec acc c = match kind_of_term c with - | Meta mv -> mv::acc - | _ -> fold_constr collrec acc c - in - collrec [] c - -let check_no_metas clenv ccl = - if occur_meta ccl then - let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m)) - (collect_meta_variables ccl) in - let metas = List.map (Evd.meta_name clenv.evd) metas in - errorlabstrm "inversion" - (str ("Cannot find an instantiation for variable"^ - (if List.length metas = 1 then " " else "s ")) ++ - prlist_with_sep pr_comma pr_name metas - (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *)) +let clear hyps = Proofview.V82.tactic (clear hyps) let var_occurs_in_pf gl id = - let env = pf_env gl in - occur_var env id (pf_concl gl) or - List.exists (occur_var_in_decl env id) (pf_hyps gl) + let env = Proofview.Goal.env gl in + occur_var env id (Proofview.Goal.concl gl) || + List.exists (occur_var_in_decl env id) (Proofview.Goal.hyps gl) (* [make_inv_predicate (ity,args) C] @@ -88,16 +65,16 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep let compute_eqn env sigma n i ai = - (ai, (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))) + (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) -let make_inv_predicate env sigma indf realargs id status concl = +let make_inv_predicate env evd indf realargs id status concl = let nrealargs = List.length realargs in let (hyps,concl) = match status with | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in - (hyps_arity,concl) + (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env id concl) then errorlabstrm "make_inv_predicate" @@ -109,41 +86,53 @@ let make_inv_predicate env sigma indf realargs id status concl = match dflt_concl with | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> - let sort = get_sort_family_of env sigma concl in - let p = make_arity env true indf (new_sort_in_family sort) in - Unification.abstract_list_all env (Evd.create_evar_defs sigma) - p concl (realargs@[mkVar id]) in + let sort = get_sort_family_of env !evd concl in + let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in + let p = make_arity env true indf sort in + let evd',(p,ptyp) = Unification.abstract_list_all env + !evd p concl (realargs@[mkVar id]) + in evd := evd'; p in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) in let nhyps = rel_context_length hyps in let env' = push_rel_context hyps env in - let realargs' = List.map (lift nhyps) realargs in - let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in (* Now the arity is pushed, and we need to construct the pairs * ai,mkRel(n-i+1) *) (* Now, we can recurse down this list, for each ai,(mkRel k) whether to push <Ai>(mkRel k)=ai (when Ai is closed). In any case, we carry along the rest of pairs *) - let rec build_concl eqns n = function - | [] -> (it_mkProd concl eqns,n) - | (ai,(xi,ti))::restlist -> + let eqdata = Coqlib.build_coq_eq_data () in + let rec build_concl eqns args n = function + | [] -> it_mkProd concl eqns, Array.rev_of_list args + | ai :: restlist -> + let ai = lift nhyps ai in + let (xi, ti) = compute_eqn env' !evd nhyps n ai in let (lhs,eqnty,rhs) = if closed0 ti then (xi,ti,ai) else - make_iterated_tuple env' sigma ai (xi,ti) + let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in + evd := sigma; res in - let eq_term = Coqlib.build_coq_eq () in - let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in - build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist + let eq_term = eqdata.Coqlib.eq in + let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in + let eqn = applist (eq,[eqnty;lhs;rhs]) in + let eqns = (Anonymous, lift n eqn) :: eqns in + let refl_term = eqdata.Coqlib.refl in + let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in + let refl = mkApp (refl_term, [|eqnty; rhs|]) in + let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in + let args = refl :: args in + build_concl eqns args (succ n) restlist in - let (newconcl,neqns) = build_concl [] 0 pairs in + let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in + let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) - (predicate,neqns) + predicate, args (* The result of the elimination is a bunch of goals like: @@ -189,13 +178,13 @@ let make_inv_predicate env sigma indf realargs id status concl = and introduces generalized hypotheis. Precondition: t=(mkVar id) *) -let rec dependent_hyps id idlist gl = +let dependent_hyps env id idlist gl = let rec dep_rec =function | [] -> [] | (id1,_,_)::l -> (* Update the type of id1: it may have been subject to rewriting *) - let d = pf_get_hyp gl id1 in - if occur_var_in_decl (Global.env()) id d + let d = pf_get_hyp id1 gl in + if occur_var_in_decl env id d then d :: dep_rec l else dep_rec l in @@ -207,8 +196,6 @@ let split_dep_and_nodep hyps gl = if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) -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 *) @@ -280,21 +267,62 @@ Summary: nine useless hypotheses! Nota: with Inversion_clear, only four useless hypotheses *) -let generalizeRewriteIntros tac depids id gls = - let dids = dependent_hyps id depids gls in - (tclTHENSEQ +let generalizeRewriteIntros as_mode tac depids id = + Proofview.tclENV >>= fun env -> + Proofview.Goal.nf_enter begin fun gl -> + let dids = dependent_hyps env id depids gl in + let reintros = if as_mode then intros_replacing else intros_possibly_replacing in + (tclTHENLIST [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 - | [] -> tclDO n (tacfun None) - | a::l -> - if n=0 then error "Too many names." - else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) + reintros (ids_of_named_context dids)]) + end + +let error_too_many_names pats = + let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in + Proofview.tclENV >>= fun env -> + tclZEROMSG ~loc ( + str "Unexpected " ++ + str (String.plural (List.length pats) "introduction pattern") ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (snd (c env Evd.empty)))) pats ++ + str ".") + +let rec get_names (allow_conj,issimple) (loc,pat as x) = match pat with + | IntroNaming IntroAnonymous | IntroForthcoming _ -> + error "Anonymous pattern not allowed for inversion equations." + | IntroNaming (IntroFresh _) -> + error "Fresh pattern not allowed for inversion equations." + | IntroAction IntroWildcard -> + error "Discarding pattern not allowed for inversion equations." + | IntroAction (IntroRewrite _) -> + error "Rewriting pattern not allowed for inversion equations." + | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, []) + | IntroAction (IntroOrAndPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l]) + when allow_conj -> (Some id,l) + | IntroAction (IntroOrAndPattern [_]) -> + if issimple then + error"Conjunctive patterns not allowed for simple inversion equations." + else + error"Nested conjunctive patterns not allowed for inversion equations." + | IntroAction (IntroInjection l) -> + error "Injection patterns not allowed for inversion equations." + | IntroAction (IntroOrAndPattern l) -> + error "Disjunctive patterns not allowed for inversion equations." + | IntroAction (IntroApplyOn (c,pat)) -> + error "Apply patterns not allowed for inversion equations." + | IntroNaming (IntroIdentifier id) -> + (Some id,[x]) + +let rec tclMAP_i allow_conj n tacfun = function + | [] -> tclDO n (tacfun (None,[])) + | a::l as l' -> + if Int.equal n 0 then error_too_many_names l' + else + tclTHEN + (tacfun (get_names allow_conj a)) + (tclMAP_i allow_conj (n-1) tacfun l) -let remember_first_eq id x = if !x = no_move then x := MoveAfter id +let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -304,217 +332,177 @@ let remember_first_eq id x = if !x = no_move then x := MoveAfter id 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 eqname names depids gls = +let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id))) (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) in - let substHypIfVariable tac id gls = - let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in + let substHypIfVariable tac id = + Proofview.Goal.nf_enter begin fun gl -> + (** We only look at the type of hypothesis "id" *) + let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in + let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in match (kind_of_term t1, kind_of_term t2) with - | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 gls - | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls - | _ -> tac id gls + | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 + | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 + | _ -> tac id + end in - let deq_trailer id neqns = - tclTHENSEQ - [(if names <> [] then clear [id] else tclIDTAC); - (tclMAP_i neqns (fun idopt -> + let deq_trailer id clear_flag _ neqns = + assert (clear_flag == None); + tclTHENLIST + [if as_mode then clear [id] else tclIDTAC; + (tclMAP_i (false,false) neqns (function (idopt,_) -> tclTRY (tclTHEN - (intro_move idopt no_move) + (intro_move_avoid idopt avoid MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) - (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false)))))) + (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) names); - (if names = [] then clear [id] else tclIDTAC)] + (if as_mode then tclIDTAC else clear [id])] + (* Doing the above late breaks the computation of dids in + generalizeRewriteIntros, and hence breaks proper intros_replacing + but it is needed for compatibility *) in substHypIfVariable (* If no immediate variable in the equation, try to decompose it *) (* and apply a trailer which again try to substitute *) (fun id -> dEqThen false (deq_trailer id) - (Some (ElimOnConstr (mkVar id,NoBindings)))) + (Some (None,ElimOnConstr (mkVar id,NoBindings)))) id - gls - -(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer - soi-meme (proposition de Valerie). *) -let rewrite_equations_gene othin neqns ba gl = - let (depids,nodepids) = split_dep_and_nodep ba.assums gl in - let rewrite_eqns = - match othin with - | Some thin -> - onLastHypId - (fun last -> - tclTHENSEQ - [tclDO neqns - (tclTHEN intro - (onLastHypId - (fun id -> - tclTRY - (projectAndApply thin id (ref no_move) - [] depids)))); - onHyps (compose List.rev (afterHyp last)) bring_hyps; - onHyps (afterHyp last) - (compose clear ids_of_named_context)]) - | None -> tclIDTAC - in - (tclTHENSEQ - [tclDO neqns intro; - bring_hyps nodepids; - clear (ids_of_named_context nodepids); - onHyps (compose List.rev (nLastDecls neqns)) bring_hyps; - onHyps (nLastDecls neqns) (compose clear ids_of_named_context); - rewrite_eqns; - tclMAP (fun (id,_,_ as d) -> - (tclORELSE (clear [id]) - (tclTHEN (bring_hyps [d]) (clear [id])))) - depids]) - gl + +let nLastDecls i tac = + Proofview.Goal.nf_enter (fun gl -> tac (nLastDecls gl i)) (* Introduction of the equations on arguments othin: discriminates Simple Inversion, Inversion and Inversion_clear None: the equations are introduced, but not rewritten Some thin: the equations are rewritten, and cleared if thin is true *) -let rec get_names allow_conj (loc,pat) = match pat with - | IntroWildcard -> - error "Discarding pattern not allowed for inversion equations." - | IntroAnonymous | IntroForthcoming _ -> - error "Anonymous pattern not allowed for inversion equations." - | IntroFresh _ -> - error "Fresh pattern not allowed for inversion equations." - | IntroRewrite _-> - error "Rewriting pattern not allowed for inversion equations." - | IntroOrAndPattern [l] -> - if allow_conj then - if l = [] then (None,[]) else - let l = List.map (fun id -> Option.get (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 no_move in - match othin with - | Some thin -> - tclTHENSEQ - [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps; - onHyps (nLastDecls neqns) (compose clear ids_of_named_context); - tclMAP_i neqns (fun o -> - let idopt,names = extract_eqn_names o in +let rewrite_equations as_mode othin neqns names ba = + Proofview.Goal.nf_enter begin fun gl -> + let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in + let first_eq = ref MoveLast in + let avoid = if as_mode then List.map pi1 nodepids else [] in + match othin with + | Some thin -> + tclTHENLIST + [tclDO neqns intro; + bring_hyps nodepids; + clear (ids_of_named_context nodepids); + (nLastDecls neqns (fun ctx -> bring_hyps (List.rev ctx))); + (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); + tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN - (intro_move idopt no_move) + (intro_move_avoid idopt avoid MoveLast) (onLastHypId (fun id -> - tclTRY (projectAndApply thin id first_eq names depids))))) + tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; - tclMAP (fun (id,_,_) gl -> - intro_move None (if thin then no_move else !first_eq) gl) + tclMAP (fun (id,_,_) -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) + let idopt = if as_mode then Some id else None in + intro_move idopt (if thin then MoveLast else !first_eq)) nodepids; - tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] - | None -> tclIDTAC - in - (tclTHENSEQ - [tclDO neqns intro; - bring_hyps nodepids; - clear (ids_of_named_context nodepids); - rewrite_eqns]) - gl + (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)] + | None -> + (* simple inversion *) + if as_mode then + tclMAP_i (false,true) neqns (fun (idopt,_) -> + intro_move idopt MoveLast) names + else + (tclTHENLIST + [tclDO neqns intro; + bring_hyps nodepids; + clear (ids_of_named_context nodepids)]) + end let interp_inversion_kind = function | SimpleInversion -> None | FullInversion -> Some false | FullInversionClear -> Some true -let rewrite_equations_tac (gene, othin) id neqns names ba = +let rewrite_equations_tac as_mode 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 names ba in - if othin = Some true (* if Inversion_clear, clear the hypothesis *) then + let tac = rewrite_equations as_mode othin neqns names ba in + match othin with + | Some true (* if Inversion_clear, clear the hypothesis *) -> tclTHEN tac (tclTRY (clear [id])) - else + | _ -> tac - -let raw_inversion inv_kind id status names gl = - let env = pf_env gl and sigma = project gl in - let c = mkVar id in - let (ind,t) = - try pf_reduce_to_atomic_ind gl (pf_type_of gl c) - with UserError _ -> - errorlabstrm "raw_inversion" - (str ("The type of "^(string_of_id id)^" is not inductive.")) in - let indclause = mk_clenv_from gl (c,t) in - let ccl = clenv_type indclause in - check_no_metas indclause ccl; - let IndType (indf,realargs) = find_rectype env sigma ccl in - let (elim_predicate,neqns) = - 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])), - case_then_using - else - Reduction.beta_appvect elim_predicate (Array.of_list realargs), - case_nodep_then_using - in - (tclTHENS - (assert_tac Anonymous cut_concl) - [case_tac names - (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) - (Some elim_predicate) ([],[]) ind indclause; - onLastHypId - (fun id -> - (tclTHEN - (apply_term (mkVar id) - (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns)) - reflexivity))]) - gl +let raw_inversion inv_kind id status names = + Proofview.Goal.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + let c = mkVar id in + let (ind, t) = + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c) + with UserError _ -> + let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in + Errors.errorlabstrm "" msg + in + let IndType (indf,realargs) = find_rectype env sigma t in + let evdref = ref sigma in + let (elim_predicate, args) = + make_inv_predicate env evdref indf realargs id status concl in + let sigma = !evdref in + let (cut_concl,case_tac) = + if status != NoDep && (dependent c concl) then + Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), + case_then_using + else + Reduction.beta_appvect elim_predicate (Array.of_list realargs), + case_nodep_then_using + in + let refined id = + let prf = mkApp (mkVar id, args) in + Proofview.Refine.refine (fun h -> h, prf) + in + let neqns = List.length realargs in + let as_mode = names != None in + tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (tclTHENS + (assert_before Anonymous cut_concl) + [case_tac names + (introCaseAssumsThen + (rewrite_equations_tac as_mode inv_kind id neqns)) + (Some elim_predicate) ind (c, t); + onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) + end (* Error messages of the inversion tactics *) -let wrap_inv_error id = function +let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> - errorlabstrm "" + Proofview.tclENV >>= fun env -> + tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort k ++ + pr_sort Evd.empty k ++ strbrk " which is not allowed for inductive definition " ++ - pr_inductive (Global.env()) i ++ str ".") - | e -> raise e + pr_inductive env (fst i) ++ str ".")) + | e -> Proofview.tclZERO ~info e (* The most general inversion tactic *) -let inversion inv_kind status names id gls = - try (raw_inversion inv_kind id status names) gls - with e when Errors.noncritical e -> wrap_inv_error id e +let inversion inv_kind status names id = + Proofview.tclORELSE + (raw_inversion inv_kind id status names) + (wrap_inv_error id) (* Specializing it... *) -let inv_gen gene thin status names = - try_intros_until (inversion (gene,thin) status names) +let inv_gen thin status names = + try_intros_until (inversion thin status names) open Tacexpr -let inv k = inv_gen false k NoDep +let inv k = inv_gen k NoDep -let half_inv_tac id = inv SimpleInversion None (NamedHyp id) let inv_tac id = inv FullInversion None (NamedHyp id) let inv_clear_tac id = inv FullInversionClear None (NamedHyp id) -let dinv k c = inv_gen false k (Dep c) +let dinv k c = inv_gen k (Dep c) -let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id) let dinv_tac id = dinv FullInversion None None (NamedHyp id) let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) @@ -522,25 +510,30 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) * perform inversion on the named hypothesis. After, it will intro them * back to their places in the hyp-list. *) -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 = - let nb_of_new_hyp = - nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init) +let invIn k names ids id = + Proofview.Goal.nf_enter begin fun gl -> + let hyps = List.map (fun id -> pf_get_hyp id gl) ids in + let concl = Proofview.Goal.concl gl in + let nb_prod_init = nb_prod concl in + let intros_replace_ids = + Proofview.Goal.enter begin fun gl -> + let concl = pf_nf_concl gl in + let nb_of_new_hyp = + nb_prod concl - (List.length hyps + nb_prod_init) + in + if nb_of_new_hyp < 1 then + intros_replacing ids + else + tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) + end in - if nb_of_new_hyp < 1 then - intros_replacing ids gls - else - tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls - in - try - (tclTHENSEQ - [bring_hyps hyps; - inversion (false,k) NoDep names id; - intros_replace_ids]) - gls - with e when Errors.noncritical e -> wrap_inv_error id e + Proofview.tclORELSE + (tclTHENLIST + [bring_hyps hyps; + inversion k NoDep names id; + intros_replace_ids]) + (wrap_inv_error id) + end let invIn_gen k names idl = try_intros_until (invIn k names idl) |