From f8f517a6e93fd02595ad96a84dec45377e92640c Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 18 Dec 2000 23:13:00 +0000 Subject: Renommages autour de NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1147 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacentries.ml | 2 +- tactics/tactics.ml | 39 +++++++++++++++++++++++++++------------ tactics/tactics.mli | 6 +++--- 3 files changed, 31 insertions(+), 16 deletions(-) (limited to 'tactics') diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml index 6c6449cda..f7afda327 100644 --- a/tactics/tacentries.ml +++ b/tactics/tacentries.ml @@ -36,7 +36,7 @@ let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep let v_specialize = hide_tactic "Specialize" dyn_new_hyp let v_elim = hide_tactic "Elim" dyn_elim let v_elimType = hide_tactic "ElimType" dyn_elim_type -let v_induction = hide_tactic "Induction" dyn_raw_induct +let v_induction = hide_tactic "Induction" dyn_old_induct let v_new_induction = hide_tactic "NewInduction" dyn_new_induct let v_case = hide_tactic "Case" dyn_case let v_caseType = hide_tactic "CaseType" dyn_case_type diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9fc785929..a75c88cfd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1053,17 +1053,23 @@ let rec recargs indpath env sigma t = ::(recargs indpath (push_rel_assum (na,t) env) sigma c2) | _ -> [] +let oldstyle = ref false + let induct_discharge indpath statuslists cname destopt avoid ra gl = let (lstatus,rstatus) = statuslists in let tophyp = ref None in let n = List.fold_left (fun n b -> if b then n+1 else n) 0 ra in - let recvarname = + let recvarname, avoid = if n=1 then - cname + cname, avoid else (* To force renumbering if there is only one *) - make_ident (string_of_id cname) (Some 1) + make_ident (string_of_id cname) (Some 1), + if !oldstyle then avoid + else (* Forbid to use cname0 *) + (make_ident (string_of_id cname) (Some 0)) :: avoid in - let hyprecname = id_of_string ("Hrec"^(string_of_id recvarname)) in + let indhyp = if !oldstyle then "Hrec" else "IH" in + let hyprecname = id_of_string (indhyp^(string_of_id recvarname)) in let rec peel_tac = function | true :: ra' -> (* For lstatus but _buggy_: if intro_gen renames @@ -1082,7 +1088,7 @@ let induct_discharge indpath statuslists cname destopt avoid ra gl = | [] -> tclIDTAC in let evaluated_peel_tac = peel_tac ra in (* because side effect on tophyp *) - let newlstatus = (* if some Hrec has taken place at the top of hyps *) + let newlstatus = (* if some IH has taken place at the top of hyps *) List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus in tclTHENLIST [ evaluated_peel_tac; @@ -1309,7 +1315,7 @@ let compute_elim_signature_and_roughly_check elimt mind = | _ -> error "Not an eliminator: some constructor case is lacking" in let _,elimt2 = decompose_prod_n (mis_nparams mis + 1) elimt in check_elim elimt2 0 - + let induction_from_context hyp0 gl = (*test suivant sans doute inutile car protégé par le letin_tac avant appel*) if List.mem hyp0 (ids_of_named_context (Global.named_context())) then @@ -1375,26 +1381,35 @@ let dyn_elim = function | l -> bad_tactic_args "elim" l (* Induction tactics *) -let raw_induct s = tclTHEN (intros_until s) (tclLAST_HYP simplest_elim) +(* This was Induction before 6.3 (induction only in quantified premisses) *) +let raw_induct s = tclTHEN (intros_until s) (tclLAST_HYP simplest_elim) let raw_induct_nodep n = tclTHEN (intros_do n) (tclLAST_HYP simplest_elim) -(* This is an hybrid of raw and new induction... seems source of confusion -let induct s = - tclORELSE (tclTHEN (intros_until s) (tclLAST_HYP simplest_elim)) - (induction_from_context s) -*) +(* This was Induction in 6.3 (hybrid form) *) +let old_induct s = tclORELSE (raw_induct s) (induction_from_context s) +let old_induct_nodep = raw_induct_nodep +(* This is Induction since V7 ("natural" induction both in quantified + premisses and introduced ones) *) let dyn_new_induct = function | [(Command c)] -> tactic_com new_induct c | [(Constr x)] -> new_induct x | [(Integer n)] -> error "Not implemented" | l -> bad_tactic_args "induct" l +(* This was Induction before 6.3 (induction only in quantified premisses) let dyn_raw_induct = function | [Identifier x] -> raw_induct x | [Integer n] -> raw_induct_nodep n | l -> bad_tactic_args "raw_induct" l +*) + +(* This was Induction in 6.3 (hybrid form) *) +let dyn_old_induct = function + | [(Identifier n)] -> old_induct n + | [Integer n] -> raw_induct_nodep n + | l -> bad_tactic_args "raw_induct" l (* Case analysis tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 335694b7c..4c1bc9770 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -167,9 +167,9 @@ val default_elim : constr * constr substitution -> tactic val simplest_elim : constr -> tactic val dyn_elim : tactic_arg list -> tactic -val raw_induct : identifier -> tactic -val raw_induct_nodep : int -> tactic -val dyn_raw_induct : tactic_arg list -> tactic +val old_induct : identifier -> tactic +val old_induct_nodep : int -> tactic +val dyn_old_induct : tactic_arg list -> tactic val dyn_new_induct : tactic_arg list -> tactic (*s Case analysis tactics. *) -- cgit v1.2.3