Experimentally adding an option for automatically erasing an

hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).

Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).

1 files changed, 15 insertions, 8 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c2403d97a..f58e218be 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -93,9 +93,13 @@ val try_intros_until :
    or a term with bindings *)
 
 val onInductionArg :
-  (constr with_bindings -> unit Proofview.tactic) ->
+  (clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
     constr with_bindings induction_arg -> unit Proofview.tactic
 
+(** Tell if a used hypothesis should be cleared by default or not *)
+
+val use_clear_hyp_by_default : unit -> bool
+
 (** {6 Introduction tactics with eliminations. } *)
 
 val intro_pattern  : Id.t move_location -> intro_pattern_expr -> unit Proofview.tactic
@@ -157,6 +161,7 @@ val unfold_constr     : global_reference -> tactic
 val clear         : Id.t list -> tactic
 val clear_body    : Id.t list -> tactic
 val keep          : Id.t list -> tactic
+val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
 val specialize    : constr with_bindings -> tactic
 
@@ -174,7 +179,7 @@ val apply                 : constr -> tactic
 val eapply                : constr -> tactic
 
 val apply_with_bindings_gen :
-  advanced_flag -> evars_flag -> constr with_bindings located list -> tactic
+  advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> tactic
 
 val apply_with_bindings   : constr with_bindings -> tactic
 val eapply_with_bindings  : constr with_bindings -> tactic
@@ -182,8 +187,8 @@ val eapply_with_bindings  : constr with_bindings -> tactic
 val cut_and_apply         : constr -> unit Proofview.tactic
 
 val apply_in :
-  advanced_flag -> evars_flag -> Id.t -> 
-    constr with_bindings located list ->
+  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+    (clear_flag * constr with_bindings located) list ->
     intro_pattern_expr located option -> unit Proofview.tactic
 
 (** {6 Elimination tactics. } *)
@@ -245,16 +250,17 @@ type eliminator = {
   elimbody : constr with_bindings
 }
 
-val general_elim  : evars_flag ->
+val general_elim  : evars_flag -> clear_flag ->
   constr with_bindings -> eliminator -> tactic
 
 val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
   clausenv -> eliminator -> unit Proofview.tactic
 
-val default_elim  : evars_flag -> constr with_bindings -> unit Proofview.tactic
+val default_elim  : evars_flag -> clear_flag -> constr with_bindings ->
+  unit Proofview.tactic
 val simplest_elim : constr -> unit Proofview.tactic
 val elim :
-  evars_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic
+  evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic
 
 val simple_induct : quantified_hypothesis -> unit Proofview.tactic
 
@@ -266,7 +272,7 @@ val induction : evars_flag ->
 
 (** {6 Case analysis tactics. } *)
 
-val general_case_analysis : evars_flag -> constr with_bindings ->  unit Proofview.tactic
+val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings ->  unit Proofview.tactic
 val simplest_case         : constr -> unit Proofview.tactic
 
 val simple_destruct          : quantified_hypothesis -> unit Proofview.tactic
@@ -384,6 +390,7 @@ module Simple : sig
   val eapply : constr -> tactic
   val elim   : constr -> unit Proofview.tactic
   val case   : constr -> unit Proofview.tactic
+  val apply_in : identifier -> constr -> unit Proofview.tactic
 
 end