changement nouvelle syntaxe (pt fixes)

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

5 files changed, 28 insertions, 23 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0e8725c6ad..046ae4ed1e 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -50,8 +50,10 @@ let h_instantiate n c =
   abstract_tactic (TacInstantiate (n,c)) (Evar_refiner.instantiate n c)
 
 (* Derived basic tactics *)
-let h_old_induction h = abstract_tactic (TacOldInduction h) (old_induct h)
-let h_old_destruct h  = abstract_tactic (TacOldDestruct h) (old_destruct h)
+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 c e idl =
   abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl)
 let h_new_destruct c e idl =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index dba9908a97..82146c01aa 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -53,8 +53,8 @@ val h_instantiate     : int -> constr -> tactic
 
 (* Derived basic tactics *)
 
-val h_old_induction   : quantified_hypothesis -> tactic
-val h_old_destruct    : quantified_hypothesis -> tactic
+val h_simple_induction   : quantified_hypothesis -> tactic
+val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
     intro_pattern_expr list list -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ccd22cc73e..7f1a0943ab 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -587,12 +587,14 @@ let rec intern_atomic lf ist x =
   | TacDAuto (n,p) -> TacDAuto (n,p)
 
   (* Derived basic tactics *)
-  | TacOldInduction h -> TacOldInduction (intern_quantified_hypothesis ist h)
+  | TacSimpleInduction h ->
+      TacSimpleInduction (intern_quantified_hypothesis ist h)
   | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
                List.map (List.map (intern_intro_pattern lf ist)) ids)
-  | TacOldDestruct h -> TacOldDestruct (intern_quantified_hypothesis ist h)
+  | TacSimpleDestruct h ->
+      TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
@@ -1602,13 +1604,14 @@ and interp_atomic ist gl = function
   | TacDAuto (n,p) -> Auto.h_dauto (n,p)
 
   (* Derived basic tactics *)
-  | TacOldInduction h ->
-      h_old_induction (interp_quantified_hypothesis ist gl h)
+  | TacSimpleInduction h ->
+      h_simple_induction (interp_quantified_hypothesis ist gl h)
   | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
         (List.map (List.map (interp_intro_pattern ist)) ids)
-  | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist gl h)
+  | TacSimpleDestruct h ->
+      h_simple_destruct (interp_quantified_hypothesis ist gl h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
@@ -1831,11 +1834,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacDAuto (n,p) -> TacDAuto (n,p)
 
   (* Derived basic tactics *)
-  | TacOldInduction h as x -> x
+  | TacSimpleInduction h as x -> x
   | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (subst_induction_arg subst c,
                option_app (subst_raw_with_bindings subst) cbo, ids)
-  | TacOldDestruct h as x -> x
+  | TacSimpleDestruct h as x -> x
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (subst_induction_arg subst c,
                option_app (subst_raw_with_bindings subst) cbo, ids)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4f9ab4ad18..f38be2f24c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1459,24 +1459,24 @@ let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
 let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
 
 (* This was Induction in 6.3 (hybrid form) *)
-let old_induct_id s =
+let simple_induct_id s =
   tclORELSE (raw_induct s) (induction_from_context true true None s [])
-let old_induct_nodep = raw_induct_nodep
+let simple_induct_nodep = raw_induct_nodep
 
-let old_induct = function
-  | NamedHyp id -> old_induct_id id
-  | AnonHyp n -> old_induct_nodep n
+let simple_induct = function
+  | NamedHyp id -> simple_induct_id id
+  | AnonHyp n -> simple_induct_nodep n
 
 (* Destruction tactics *)
 
-let old_destruct_id s    =
+let simple_destruct_id s    =
   (tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case))
-let old_destruct_nodep n =
+let simple_destruct_nodep n =
   (tclTHEN (intros_until_n n)    (tclLAST_HYP simplest_case))
 
-let old_destruct = function
-  | NamedHyp id -> old_destruct_id id
-  | AnonHyp n -> old_destruct_nodep n
+let simple_destruct = function
+  | NamedHyp id -> simple_destruct_id id
+  | AnonHyp n -> simple_destruct_nodep n
 
 (*
  *  Eliminations giving the type instead of the proof.
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 38c31f0159..1f4c5b35cf 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -172,7 +172,7 @@ val elim          : constr with_bindings -> constr with_bindings option -> tacti
 val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
-val old_induct     : quantified_hypothesis -> tactic
+val simple_induct     : quantified_hypothesis -> tactic
 val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
@@ -184,7 +184,7 @@ val new_induct : constr induction_arg -> constr with_bindings option ->
 val general_case_analysis : constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
 
-val old_destruct          : quantified_hypothesis -> tactic
+val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
   intro_pattern_expr list list -> tactic