Renommages autour de NewInduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1147 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 31 insertions, 16 deletions

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. *)