diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 7 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/hiddentac.ml | 25 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 10 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 69 | ||||
| -rw-r--r-- | tactics/tactics.ml | 107 | ||||
| -rw-r--r-- | tactics/tactics.mli | 8 |
8 files changed, 148 insertions, 82 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index c4b7ad13c..133524ba7 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Util open Pp @@ -261,7 +261,8 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere) + (thin_body [id]) gls in tclMAP add_aux items gls let prepare_goal items gls = @@ -807,7 +808,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac true (Name id) t Tacexpr.nowhere gls + letin_tac None (Name id) t Tacexpr.nowhere gls (* tactics for reconsider *) diff --git a/tactics/equality.ml b/tactics/equality.ml index b8e868f37..b0c5a29eb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1181,7 +1181,7 @@ let subst_one x gl = let introtac = function (id,None,_) -> intro_using id | (id,Some hval,htyp) -> - letin_tac true (Name id) + letin_tac None (Name id) (mkCast(replace_term varx rhs hval,DEFAULTcast, replace_term varx rhs htyp)) nowhere in diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index a9a8da193..bb279b5ba 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -75,5 +75,5 @@ let let_evar name typ gls = let evd = Evd.create_goal_evar_defs gls.sigma in let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd')) - (Tactics.letin_tac true name evar nowhere) gls + (Tactics.letin_tac None name evar nowhere) gls diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index c3b7e0a8b..0a9ed111f 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -61,13 +61,16 @@ let h_mutual_cofix b id l = (mutual_cofix id l) let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c) -let h_generalize cl = - abstract_tactic (TacGeneralize (List.map inj_open cl)) - (generalize cl) +let h_generalize_gen cl = + abstract_tactic (TacGeneralize (List.map (on_fst inj_occ) cl)) + (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) +let h_generalize cl = + h_generalize_gen (List.map (fun c -> (([],c),Names.Anonymous)) cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) -let h_let_tac na c cl = - abstract_tactic (TacLetTac (na,inj_open c,cl)) (letin_tac true na c cl) +let h_let_tac b na c cl = + let with_eq = if b then None else Some true in + abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c cl) let h_instantiate n c ido = (Evar_tactics.instantiate n c ido) (* abstract_tactic (TacInstantiate (n,c,cls)) @@ -78,12 +81,12 @@ let h_simple_induction h = abstract_tactic (TacSimpleInduction h) (simple_induct h) let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) -let h_new_induction ev c e idl = - abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) - (new_induct ev c e idl) -let h_new_destruct ev c e idl = - abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) - (new_destruct ev c e idl) +let h_new_induction ev c e idl cl = + abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl,cl)) + (new_induct ev c e idl cl) +let h_new_destruct ev c e idl cl = + abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl,cl)) + (new_destruct ev c e idl cl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 49415649b..bb88518c9 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -52,8 +52,10 @@ val h_cofix : identifier option -> tactic val h_cut : constr -> tactic val h_generalize : constr list -> tactic +val h_generalize_gen : (constr with_occurrences * name) list -> tactic val h_generalize_dep : constr -> tactic -val h_let_tac : name -> constr -> Tacticals.clause -> tactic +val h_let_tac : letin_flag -> name -> constr -> + Tacticals.clause -> tactic val h_instantiate : int -> Rawterm.rawconstr -> (identifier * hyp_location_flag, unit) location -> tactic @@ -63,10 +65,12 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_new_induction : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> + Tacticals.clause option -> tactic val h_new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> + Tacticals.clause option -> tactic val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 58d7e358c..5fb45299f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -587,15 +587,15 @@ let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) let intern_flag ist red = { red with rConst = List.map (intern_evaluable ist) red.rConst } -let intern_constr_occurrence ist (l,c) = (l,intern_constr ist c) +let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) let intern_red_expr ist = function | Unfold l -> Unfold (List.map (intern_unfold ist) l) | Fold l -> Fold (List.map (intern_constr ist) l) | Cbv f -> Cbv (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) - | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) - | Simpl o -> Simpl (Option.map (intern_constr_occurrence ist) o) + | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) + | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r @@ -711,12 +711,15 @@ let rec intern_atomic lf ist x = TacAssert (Option.map (intern_tactic ist) otac, intern_intro_pattern lf ist ipat, intern_constr_gen (otac<>None) ist c) - | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) + | TacGeneralize cl -> + TacGeneralize (List.map (fun (c,na) -> + intern_constr_with_occurrences ist c, + intern_name lf ist na) cl) | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) - | TacLetTac (na,c,cls) -> + | TacLetTac (na,c,cls,b) -> let na = intern_name lf ist na in TacLetTac (na,intern_constr ist c, - (clause_app (intern_hyp_location ist) cls)) + (clause_app (intern_hyp_location ist) cls),b) (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l) @@ -734,16 +737,18 @@ let rec intern_atomic lf ist x = (* Derived basic tactics *) | TacSimpleInduction h -> TacSimpleInduction (intern_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids) -> + | TacNewInduction (ev,lc,cbo,ids,cls) -> TacNewInduction (ev,List.map (intern_induction_arg ist) lc, Option.map (intern_constr_with_bindings ist) cbo, - (intern_intro_pattern lf ist ids)) + intern_intro_pattern lf ist ids, + Option.map (clause_app (intern_hyp_location ist)) cls) | TacSimpleDestruct h -> TacSimpleDestruct (intern_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids) -> + | TacNewDestruct (ev,c,cbo,ids,cls) -> TacNewDestruct (ev,List.map (intern_induction_arg ist) c, Option.map (intern_constr_with_bindings ist) cbo, - (intern_intro_pattern lf ist ids)) + intern_intro_pattern lf ist ids, + Option.map (clause_app (intern_hyp_location ist)) cls) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in @@ -777,7 +782,7 @@ let rec intern_atomic lf ist x = | TacReduce (r,cl) -> TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> - TacChange (Option.map (intern_constr_occurrence ist) occl, + TacChange (Option.map (intern_constr_with_occurrences ist) occl, (if occl = None & cl.onhyps = None & cl.concl_occs = [] then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) @@ -1462,7 +1467,8 @@ let interp_flag ist env red = let interp_pattern ist sigma env (l,c) = (interp_int_or_var_list ist l, interp_constr ist sigma env c) -let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl) +let pf_interp_constr_with_occurrences ist gl = + interp_pattern ist (project gl) (pf_env gl) let interp_red_expr ist sigma env = function | Unfold l -> Unfold (List.map (interp_unfold ist env) l) @@ -2072,11 +2078,15 @@ and interp_atomic ist gl = function abstract_tactic (TacAssert (t,ipat,inj_open c)) (Tactics.forward (Option.map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) - | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl) + | TacGeneralize cl -> + h_generalize_gen + (List.map (fun (c,na) -> + pf_interp_constr_with_occurrences ist gl c, + interp_fresh_name ist gl na) cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) - | TacLetTac (na,c,clp) -> + | TacLetTac (na,c,clp,b) -> let clp = interp_clause ist gl clp in - h_let_tac (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp + h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp (* Automation tactics *) | TacTrivial (lems,l) -> @@ -2097,16 +2107,18 @@ and interp_atomic ist gl = function (* Derived basic tactics *) | TacSimpleInduction h -> h_simple_induction (interp_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids) -> + | TacNewInduction (ev,lc,cbo,ids,cls) -> h_new_induction ev (List.map (interp_induction_arg ist gl) lc) (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) + (Option.map (interp_clause ist gl) cls) | TacSimpleDestruct h -> h_simple_destruct (interp_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids) -> + | TacNewDestruct (ev,c,cbo,ids,cls) -> h_new_destruct ev (List.map (interp_induction_arg ist gl) c) (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) + (Option.map (interp_clause ist gl) cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2145,7 +2157,7 @@ and interp_atomic ist gl = function | TacReduce (r,cl) -> h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> - h_change (Option.map (pf_interp_pattern ist gl) occl) + h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl) (if occl = None & cl.onhyps = None & cl.concl_occs = [] then pf_interp_type ist gl c else pf_interp_constr ist gl c) @@ -2351,15 +2363,15 @@ let subst_unfold subst (l,e) = let subst_flag subst red = { red with rConst = List.map (subst_evaluable subst) red.rConst } -let subst_constr_occurrence subst (l,c) = (l,subst_rawconstr subst c) +let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c) let subst_redexp subst = function | Unfold l -> Unfold (List.map (subst_unfold subst) l) | Fold l -> Fold (List.map (subst_rawconstr subst) l) | Cbv f -> Cbv (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) - | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) - | Simpl o -> Simpl (Option.map (subst_constr_occurrence subst) o) + | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) + | Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let subst_raw_may_eval subst = function @@ -2401,9 +2413,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacCut c -> TacCut (subst_rawconstr subst c) | TacAssert (b,na,c) -> TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c) - | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) + | TacGeneralize cl -> + TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) - | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) + | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_rawconstr subst c,clp,b) (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l) @@ -2416,13 +2429,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Derived basic tactics *) | TacSimpleInduction h as x -> x - | TacNewInduction (ev,lc,cbo,ids) -> + | TacNewInduction (ev,lc,cbo,ids,cls) -> TacNewInduction (ev,List.map (subst_induction_arg subst) lc, - Option.map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids, cls) | TacSimpleDestruct h as x -> x - | TacNewDestruct (ev,c,cbo,ids) -> + | TacNewDestruct (ev,c,cbo,ids,cls) -> TacNewDestruct (ev,List.map (subst_induction_arg subst) c, - Option.map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids, cls) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2449,7 +2462,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (occl,c,cl) -> - TacChange (Option.map (subst_constr_occurrence subst) occl, + TacChange (Option.map (subst_constr_with_occurrences subst) occl, subst_rawconstr subst c, cl) (* Equivalence relations *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9812b5f82..c81d7f317 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1131,24 +1131,50 @@ let true_cut = assert_tac true (* Generalize tactics *) (**************************) -let generalize_goal gl c cl = +let generalized_name c t cl = function + | Name id as na -> na + | Anonymous -> + match kind_of_term c with + | Var id -> + (* Keep the name even if not occurring: may be used by intros later *) + Name id + | _ -> + if noccurn 1 cl then Anonymous else + (* On ne s'etait pas casse la tete : on avait pris pour nom de + variable la premiere lettre du type, meme si "c" avait ete une + constante dont on aurait pu prendre directement le nom *) + named_hd (Global.env()) t Anonymous + +let generalize_goal gl i ((occs,c),na) cl = let t = pf_type_of gl c in - match kind_of_term c with + let decls,cl = decompose_prod_n_assum i cl in + let dummy_prod = it_mkProd_or_LetIn mkProp decls in + let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in + let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in + let na = generalized_name c t cl' na in + mkProd (na,t,cl') + +(* + match kind_of_term cl with + | App (f,[|a|]) when isLambda f & eq_constr a c -> + (* Assume tactic pattern has been applied first *) + let na = match kind_of_term c with Var id -> Name id | _ -> Anonymous in + mkProd_name (pf_env gl) (na,t,mkApp (f,[|mkRel 1|])) + | _ -> + match kind_of_term c with | Var id -> (* The choice of remembering or not a non dependent name has an impact on the future Intro naming strategy! *) (* if dependent c cl then mkNamedProd id t cl else mkProd (Anonymous,t,cl) *) - mkNamedProd id t cl + mkNamedProd id t cl | _ -> let cl' = subst_term c cl in if noccurn 1 cl' then mkProd (Anonymous,t,cl) - (* On ne se casse pas la tete : on prend pour nom de variable - la premiere lettre du type, meme si "ci" est une - constante et qu'on pourrait prendre directement son nom *) - else - prod_name (Global.env()) (Anonymous, t, cl') + else + mkProd_name (pf_env gl) (Anonymous, t, cl') +*) let generalize_dep c gl = let env = pf_env gl in @@ -1171,16 +1197,19 @@ let generalize_dep c gl = | _ -> tothin in let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in - let cl'' = generalize_goal gl c cl' in + let cl'' = generalize_goal gl 0 (([],c),Anonymous) cl' in let args = Array.to_list (instance_from_named_context to_quantify_rev) in tclTHEN (apply_type cl'' (c::args)) (thin (List.rev tothin')) gl - -let generalize lconstr gl = - let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in - apply_type newcl lconstr gl + +let generalize_gen lconstr gl = + let newcl = + list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in + apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl + +let generalize l = generalize_gen (List.map (fun c -> (([],c),Anonymous)) l) let revert hyps gl = tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl @@ -1203,7 +1232,7 @@ let quantify lconstr = [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms [...x1:T1(c),...,x2:T2(c),... |- G(c)] into - [...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or + [...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted; @@ -1325,11 +1354,21 @@ let letin_tac with_eq name c occs gl = error ("The variable "^(string_of_id x)^" is already declared") in let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in let t = pf_type_of gl c in - let newcl = mkNamedLetIn id c t ccl in + let newcl,eq_tac = match with_eq with + | Some lr -> + let heq = fresh_id [] (add_prefix "Heq" id) gl in + let eqdata = build_coq_eq_data () in + let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in + let eq = applist (eqdata.eq,args) in + let refl = applist (eqdata.refl, [t;mkVar id]) in + mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)), + tclTHEN (intro_gen (IntroMustBe heq) lastlhyp true) (thin_body [heq;id]) + | None -> + mkNamedLetIn id c t ccl, tclIDTAC in tclTHENLIST [ convert_concl_no_check newcl DEFAULTcast; intro_gen (IntroMustBe id) lastlhyp true; - if with_eq then tclIDTAC else thin_body [id]; + eq_tac; tclMAP convert_hyp_no_check depdecls ] gl (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) @@ -1506,14 +1545,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl = | Var id -> let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) (mkVar id) allClauses) + (letin_tac None (Name x) (mkVar id) allClauses) (atomize_one (i-1) ((mkVar x)::avoid)) gl | _ -> let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) c allClauses) + (letin_tac None (Name x) c allClauses) (atomize_one (i-1) ((mkVar x)::avoid)) gl else tclIDTAC gl @@ -2439,18 +2478,19 @@ let induction_without_atomization isrec with_evars elim names lid gl = then error "Not the right number of induction arguments" else induction_from_context_l isrec with_evars elim_info lid names gl -let new_induct_gen isrec with_evars elim names (c,lbind) gl = +let new_induct_gen isrec with_evars elim names (c,lbind) cls gl = match kind_of_term c with | Var id when not (mem_named_context id (Global.named_context())) - & lbind = NoBindings & not with_evars -> + & lbind = NoBindings & not with_evars & cls = None -> induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) gl | _ -> let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let id = fresh_id [] x gl in + let with_eq = if cls <> None then Some (not (isVar c)) else None in tclTHEN - (letin_tac true (Name id) c allClauses) + (letin_tac with_eq (Name id) c (Option.default allClauses cls)) (induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind)) gl @@ -2467,7 +2507,8 @@ let new_induct_gen_l isrec with_evars elim names lc gl = | [] -> tclIDTAC gl | c::l' -> match kind_of_term c with - | Var id when not (mem_named_context id (Global.named_context())) -> + | Var id when not (mem_named_context id (Global.named_context())) + & not with_evars -> let _ = newlc:= id::!newlc in atomize_list l' gl @@ -2480,7 +2521,7 @@ let new_induct_gen_l isrec with_evars elim names lc gl = let _ = newlc:=id::!newlc in let _ = letids:=id::!letids in tclTHEN - (letin_tac true (Name id) c allClauses) + (letin_tac None (Name id) c allClauses) (atomize_list newl') gl in tclTHENLIST [ @@ -2495,10 +2536,10 @@ let new_induct_gen_l isrec with_evars elim names lc gl = gl -let induct_destruct_l isrec with_evars lc elim names = +let induct_destruct_l isrec with_evars lc elim names cls = (* Several induction hyps: induction scheme is mandatory *) let _ = - if elim = None + if elim = None then error ("Induction scheme must be given when several induction hypothesis.\n" ^ "Example: induction x1 x2 x3 using my_scheme.") in @@ -2509,6 +2550,9 @@ let induct_destruct_l isrec with_evars lc elim names = | ElimOnConstr (x,NoBindings) -> x | _ -> error "don't know where to find some argument") lc in + if cls <> None then + error + "'in' clause not supported when several induction hypothesis are given"; new_induct_gen_l isrec with_evars elim names newlc @@ -2517,27 +2561,28 @@ let induct_destruct_l isrec with_evars lc elim names = principles). TODO: really unify induction with one and induction with several args *) -let induct_destruct isrec with_evars lc elim names = +let induct_destruct isrec with_evars lc elim names cls = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) if List.length lc = 1 then (* induction on one arg: use old mechanism *) try let c = List.hd lc in match c with - | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c + | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c cls | ElimOnAnonHyp n -> tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> - new_induct_gen isrec with_evars elim names (c,NoBindings))) + new_induct_gen isrec with_evars elim names (c,NoBindings) cls)) (* Identifier apart because id can be quantified in goal and not typable *) | ElimOnIdent (_,id) -> tclTHEN (tclTRY (intros_until_id id)) - (new_induct_gen isrec with_evars elim names (mkVar id,NoBindings)) + (new_induct_gen isrec with_evars elim names + (mkVar id,NoBindings) cls) with (* If this fails, try with new mechanism but if it fails too, then the exception is the first one. *) | x -> - (try induct_destruct_l isrec with_evars lc elim names + (try induct_destruct_l isrec with_evars lc elim names cls with _ -> raise x) - else induct_destruct_l isrec with_evars lc elim names + else induct_destruct_l isrec with_evars lc elim names cls diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1b2b7b38f..bfb49cba7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -251,7 +251,7 @@ val elim : val simple_induct : quantified_hypothesis -> tactic val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic (*s Case analysis tactics. *) @@ -260,7 +260,7 @@ val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic (*s Eliminations giving the type instead of the proof. *) @@ -323,11 +323,11 @@ val cut_in_parallel : constr list -> tactic val assert_as : bool -> intro_pattern_expr -> constr -> tactic val forward : tactic option -> intro_pattern_expr -> constr -> tactic - +val letin_tac : bool option -> name -> constr -> clause -> tactic val true_cut : name -> constr -> tactic -val letin_tac : bool -> name -> constr -> clause -> tactic val assert_tac : bool -> name -> constr -> tactic val generalize : constr list -> tactic +val generalize_gen : ((int list * constr) * name) list -> tactic val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic |