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

4 files changed, 22 insertions, 17 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 39bdda79bd..66b016cfce 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -16,8 +16,7 @@ open Util
 GEXTEND Gram
 
   identarg:
-    [ [ id = IDENT -> <:ast< ($VAR $id) >> 
-      | id = METAIDENT -> <:ast< ($VAR $id) >> ] ]
+    [ [ id = Constr.ident -> id ] ]
   ;
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> ] ]
@@ -311,6 +310,8 @@ GEXTEND Gram
           <:ast< (Cofix $id ($LIST $fd)) >>
       | IDENT "Induction"; s = identarg -> <:ast< (Induction $s) >>
       | IDENT "Induction"; n = numarg -> <:ast< (Induction $n) >>
+      | IDENT "NewInduction"; c = constrarg -> <:ast< (NewInduction $c) >>
+      | IDENT "NewInduction"; n = numarg -> <:ast< (NewInduction $n) >>
       | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg ->
           <:ast< (DoubleInd $i $j) >>
       | IDENT "Trivial" -> <:ast<(Trivial)>>
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. *)