Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)

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

1 files changed, 3 insertions, 5 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f3da4a8c9..91c6731b7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -175,11 +175,10 @@ val general_elim_in :
 val default_elim  : constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
 val elim          : constr with_bindings -> constr with_bindings option -> tactic
-val simple_induct     : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
+val simple_induct : quantified_hypothesis -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-  -> tactic
+  intro_pattern_expr option -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -188,8 +187,7 @@ val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-  -> tactic
+  intro_pattern_expr option -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)