Distinction claire entre Induction (nom interne : raw_induct) et le nouvel induction (now temporaire NewInduction)

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

3 files changed, 19 insertions, 15 deletions

diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index 90003dc344..5b1232feb7 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -36,7 +36,8 @@ 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_induct
+let v_induction     = hide_tactic "Induction"     dyn_raw_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
 let v_destruct      = hide_tactic "Destruct"      dyn_destruct
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c71abe264d..6d3da97ad0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1359,24 +1359,26 @@ let dyn_elim = function
   | l -> bad_tactic_args "elim" l
 	
 (* Induction tactics *)
+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)
+*)
 
-let induct_nodep n = tclTHEN (intros_do n) (tclLAST_HYP simplest_elim)
-
-(* Pour le futur
-let dyn_induct = function
-  | [(Command c)] -> tactic_com new_induct x
+let dyn_new_induct = function
+  | [(Command c)] -> tactic_com new_induct c
   | [(Constr x)]  -> new_induct x
-  | [(Integer n)] -> induct_nodep n
+  | [(Integer n)] -> error "Not implemented"
   | l             -> bad_tactic_args "induct" l
-*)
 
-let dyn_induct = function 
-  | [Identifier x] -> induct x
-  | [Integer n]    -> induct_nodep n
-  | l              -> bad_tactic_args "induct" l
+let dyn_raw_induct = function 
+  | [Identifier x] -> raw_induct x
+  | [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 ada02fcf22..03ab3a2738 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -167,9 +167,10 @@ val default_elim   : constr * constr substitution -> tactic
 val simplest_elim  : constr -> tactic
 val dyn_elim       : tactic_arg list -> tactic
 
-val induct         : identifier -> tactic
-val induct_nodep   : int        -> tactic
-val dyn_induct     : tactic_arg list -> tactic
+val raw_induct       : identifier -> tactic
+val raw_induct_nodep : int        -> tactic
+val dyn_raw_induct : tactic_arg list -> tactic
+val dyn_new_induct : tactic_arg list -> tactic
 
 (*s Case analysis tactics. *)