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).

22 files changed, 349 insertions, 199 deletions

diff --git a/CHANGES b/CHANGES
index e3aa5d792..00f15a62a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -173,6 +173,8 @@ Tactics
 - The good bullet (-/+/*) is suggested sometimes when user gives a wrong one.
 - New tactic "enough", symmetric to "assert", but with subgoals
   swapped, as a more friendly replacement of "cut".
+- In destruct/induction, experimental modifier "!" prefixing the
+  hypothesis name to tell not erasing the hypothesis.
 
 Program
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 28d854eaa..a3953bb96 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1573,6 +1573,14 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
+\item{\tt destruct !{\ident}}
+
+  This is a case when the destructed term is an hypothesis of the
+  context. The ``!'' modifier tells to keep the hypothesis in the
+  context after destruction.
+
+  This applies also to the other form of {\tt destruct} and {\tt edestruct}.
+
 \item{\tt case \term}\label{case}\tacindex{case}
 
   The tactic {\tt case} is a more basic tactic to perform case
@@ -1750,6 +1758,15 @@ induction n.
   einduction}.  It combines the effects of the {\tt with}, {\tt as},
   {\tt eqn:}, {\tt using}, and {\tt in} clauses.
 
+\item{\tt induction !{\ident}}
+
+  This is a case when the term on which to apply induction is an
+  hypothesis of the context. The ``!'' modifier tells to keep the
+  hypothesis in the context after induction.
+
+  This applies also to the other form of {\tt induction} and {\tt
+    einduction}.
+
 \item {\tt elim \term}\label{elim}
 
   This is a more basic induction tactic.  Again, the type of the
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 2690cf867..4fede761f 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -247,6 +247,9 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
 let mlexpr_of_constr_with_binding =
   mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
 
+let mlexpr_of_constr_with_binding_arg =
+  mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) mlexpr_of_constr_with_binding
+
 let mlexpr_of_move_location f = function
   | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >>
   | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >>
@@ -309,13 +312,13 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacExact c ->
       <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply (b,false,cb,None) ->
-      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
+      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding_arg cb$ None >>
   | Tacexpr.TacElim (false,cb,cbo) ->
-      let cb = mlexpr_of_constr_with_binding cb in
+      let cb = mlexpr_of_constr_with_binding_arg cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       <:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
   | Tacexpr.TacCase (false,cb) ->
-      let cb = mlexpr_of_constr_with_binding cb in
+      let cb = mlexpr_of_constr_with_binding_arg cb in
       <:expr< Tacexpr.TacCase False $cb$ >>
   | Tacexpr.TacFix (ido,n) ->
       let ido = mlexpr_of_ident_option ido in
@@ -364,7 +367,9 @@ let rec mlexpr_of_atomic_tactic = function
 	$mlexpr_of_triple
 	(mlexpr_of_list
 	   (mlexpr_of_pair
-	      mlexpr_of_induction_arg
+              (mlexpr_of_pair
+                 (mlexpr_of_option mlexpr_of_bool)
+	         mlexpr_of_induction_arg)
 	      (mlexpr_of_pair
 		 (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
 		 (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4174de123..0c5eed714 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -25,14 +25,18 @@ type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
 type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
 
-type 'a induction_arg =
+type 'a core_induction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of Id.t located
   | ElimOnAnonHyp of int
 
+type 'a induction_arg =
+  clear_flag * 'a core_induction_arg
+
 type inversion_kind =
   | SimpleInversion
   | FullInversion
@@ -62,6 +66,8 @@ type ('constr,'id) induction_clause_list =
     * 'constr with_bindings option (* using ... *)
     * 'id clause_expr option (* in ... *)
 
+type 'a with_bindings_arg = clear_flag * 'a with_bindings
+
 type multi =
   | Precisely of int
   | UpTo of int
@@ -108,10 +114,10 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
-  | TacApply of advanced_flag * evars_flag * 'trm with_bindings list *
-      ('nam * intro_pattern_expr located option) option
-  | TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option
-  | TacCase of evars_flag * 'trm with_bindings
+  | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
+      (clear_flag * 'nam * intro_pattern_expr located option) option
+  | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
+  | TacCase of evars_flag * 'trm with_bindings_arg
   | TacFix of Id.t option * int
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacCofix of Id.t option
@@ -157,7 +163,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'trm with_bindings) list * 'nam clause_expr *
+      (bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr *
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c02f2d569..3c097db1c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -136,19 +136,19 @@ let induction_arg_of_constr (c,lbind as clbind) = match lbind with
   | _ -> ElimOnConstr clbind
 
 let mkTacCase with_evar = function
-  | [ElimOnConstr cl,(None,None)],None,None ->
-      TacCase (with_evar,cl)
+  | [(clear,ElimOnConstr cl),(None,None)],None,None ->
+      TacCase (with_evar,(clear,cl))
   (* Reinterpret numbers as a notation for terms *)
-  | [ElimOnAnonHyp n,(None,None)],None,None ->
+  | [(clear,ElimOnAnonHyp n),(None,None)],None,None ->
       TacCase (with_evar,
-        (CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
-	 NoBindings))
+        (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
+	 NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
-  | [ElimOnIdent id,(None,None)],None,None ->
-      TacCase (with_evar,(CRef (Ident id,None),NoBindings))
+  | [(clear,ElimOnIdent id),(None,None)],None,None ->
+      TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings)))
   | ic ->
-      if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic)
+      if List.exists (function ((_, ElimOnAnonHyp _),_) -> true | _ -> false) (pi1 ic)
       then
 	error "Use of numbers as direct arguments of 'case' is not supported.";
       TacInductionDestruct (false,with_evar,ic)
@@ -237,10 +237,15 @@ GEXTEND Gram
     [ [ c = constr -> c ] ]
   ;
   induction_arg:
-    [ [ n = natural -> ElimOnAnonHyp n
-      | c = constr_with_bindings -> induction_arg_of_constr c
+    [ [ n = natural -> (None,ElimOnAnonHyp n)
+      | c = constr_with_bindings -> (None,induction_arg_of_constr c)
+      | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c)
     ] ]
   ;
+  constr_with_bindings_arg:
+    [ [ ">"; c = constr_with_bindings -> (Some true,c)
+      | c = constr_with_bindings -> (None,c) ] ]
+  ;
   quantified_hypothesis:
     [ [ id = ident -> NamedHyp id
       | n = natural -> AnonHyp n ] ]
@@ -412,7 +417,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   in_hyp_as:
-    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
+    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat)
       | -> None ] ]
   ;
   orient:
@@ -496,12 +501,12 @@ GEXTEND Gram
     [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
   ;
   rewriter :
-    [ [ "!"; c = constr_with_bindings -> (RepeatPlus,c)
-      | ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c)
-      | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
-      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings -> (UpTo n,c)
-      | n = natural; c = constr_with_bindings -> (Precisely n,c)
-      | c = constr_with_bindings -> (Precisely 1, c)
+    [ [ "!"; c = constr_with_bindings -> (RepeatPlus,(None,c))
+      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
+      | n = natural; "!"; c = constr_with_bindings -> (Precisely n,(None,c))
+      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
+      | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
+      | c = constr_with_bindings -> (Precisely 1, (None,c))
       ] ]
   ;
   oriented_rewriter :
@@ -534,17 +539,19 @@ GEXTEND Gram
 
       | IDENT "exact"; c = constr -> TacExact c
 
-      | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+      | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
-      | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ",";
+      | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp)
-      | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+      | IDENT "simple"; IDENT "apply";
+          cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp)
-      | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP",";
+      | IDENT "simple"; IDENT "eapply";
+          cl = LIST1 constr_with_bindings_arg SEP",";
           inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp)
-      | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
+      | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
           TacElim (false,cl,el)
-      | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
+      | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
           TacElim (true,cl,el)
       | IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
       | IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 4218286b0..f780d1bb5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -721,7 +721,7 @@ let rec consider_match may_intro introduced available expected gls =
 		 try conjunction_arity id gls with
 		     Not_found -> error "Matching hypothesis not found." in
 		 tclTHENLIST
-		   [Proofview.V82.of_tactic (general_case_analysis false (mkVar id,NoBindings));
+		   [Proofview.V82.of_tactic (simplest_case (mkVar id));
 		    intron_then nhyps []
 		      (fun l -> consider_match may_intro introduced
 			 (List.rev_append l rest_ids) expected)] gls)
@@ -1313,7 +1313,7 @@ let end_tac et2 gls =
 	      tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)]
 	  | ET_Case_analysis,EK_nodep ->
 	      tclTHEN
-		(Proofview.V82.of_tactic (general_case_analysis false (pi.per_casee,NoBindings)))
+		(Proofview.V82.of_tactic (simplest_case pi.per_casee))
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 841796ed7..1981fb837 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -976,7 +976,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (general_case_analysis false (mkVar rec_id,NoBindings)));
+	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 808b2604c..953e1f049 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -80,7 +80,7 @@ let functional_induction with_clean c princl pat =
 	if princ_infos.Tactics.farg_in_concl
 	then [c] else []
       in
-      List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list)
+      List.map (fun c -> None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list)
     in
     let princ' = Some (princ,bindings) in
     let princ_vars =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 52d3b4a87..5682c2aa4 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -799,7 +799,7 @@ and intros_with_rewrite_aux : tactic =
 		      Proofview.V82.of_tactic Tauto.tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings));
+			Proofview.V82.of_tactic (simplest_case v);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -836,7 +836,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings));
+	      Proofview.V82.of_tactic (simplest_case v);
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -855,7 +855,7 @@ let rec reflexivity_with_destruct_cases g =
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp id);thin [id];intros_with_rewrite]  g
+		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
@@ -1013,7 +1013,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index dbf83936a..7738f0c53 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -120,9 +120,15 @@ let pr_bindings_no_with prc prlc = function
         prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
   | NoBindings -> mt ()
 
+let pr_keep keep pp x =
+  (if keep then str "!" else mt()) ++ pp x
+
 let pr_with_bindings prc prlc (c,bl) =
   prc c ++ hv 0 (pr_bindings prc prlc bl)
 
+let pr_with_bindings_arg prc prlc (keep,c) =
+  pr_keep keep (pr_with_bindings prc prlc) c
+
 let pr_with_constr prc = function
   | None -> mt ()
   | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
@@ -575,6 +581,7 @@ let make_pr_tac pr_tac_level
 let pr_bindings = pr_bindings pr_lconstr pr_constr in
 let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
 let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
+let pr_with_bindings_arg = pr_with_bindings_arg pr_lconstr pr_constr in
 let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level pr_pat in
 let pr_alias = pr_alias pr_constr pr_lconstr pr_tac_level pr_pat in
 let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst,pr_pat) in
@@ -667,13 +674,13 @@ and pr_atom1 = function
   | TacApply (a,ev,cb,inhyp) ->
       hov 1 ((if a then mt() else str "simple ") ++
              str (with_evars ev "apply") ++ spc () ++
-             prlist_with_sep pr_comma pr_with_bindings cb ++
+             prlist_with_sep pr_comma pr_with_bindings_arg cb ++
              pr_in_hyp_as pr_ident inhyp)
   | TacElim (ev,cb,cbo) ->
-      hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
+      hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++
         pr_opt pr_eliminator cbo)
   | TacCase (ev,cb) ->
-      hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
+      hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
       hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
@@ -722,8 +729,8 @@ and pr_atom1 = function
   | TacInductionDestruct (isrec,ev,(l,el,cl)) ->
       hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
              spc () ++
-             prlist_with_sep pr_comma (fun (h,ids) ->
-	       pr_induction_arg pr_lconstr pr_constr h ++
+             prlist_with_sep pr_comma (fun ((keep,h),ids) ->
+	       pr_keep keep (pr_induction_arg pr_lconstr pr_constr) h ++
 	       pr_with_induction_names ids) l ++
              pr_opt pr_eliminator el ++
 	     pr_opt_no_spc (pr_clauses None pr_ident) cl)
@@ -800,7 +807,7 @@ and pr_atom1 = function
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
 	     (fun (b,m,c) ->
-		pr_orient b ++ pr_multi m ++ pr_with_bindings c)
+		pr_orient b ++ pr_multi m ++ pr_with_bindings_arg c)
 	     l
 	     ++ pr_clauses (Some true) pr_ident cl
 	     ++	(match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt()))
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 805ecc3eb..96e8e60bb 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -94,7 +94,9 @@ let contradiction_term (c,lbind as cl) =
     let typ = type_of c in
     let _, ccl = splay_prod env sigma typ in
     if is_empty_type ccl then
-      Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
+      Tacticals.New.tclTHEN
+        (elim false None cl None)
+        (Tacticals.New.tclTRY assumption)
     else
       Proofview.tclORELSE
         begin
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a23ae4e82..7343aa532 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -460,6 +460,17 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   do_hyps
 
+let apply_special_clear_request clear_flag f =
+  Proofview.Goal.raw_enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try
+      let sigma,(c,bl) = f env sigma in
+      apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
+    with
+      e when catchable_exception e -> tclIDTAC
+  end
+
 type delayed_open_constr_with_bindings =
     env -> evar_map -> evar_map * constr with_bindings
 
@@ -484,7 +495,9 @@ let general_multi_multi_rewrite with_evars l cl tac =
   in
   let rec loop = function
     | [] -> Proofview.tclUNIT ()
-    | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
+    | (l2r,m,clear_flag,c)::l ->
+        tclTHENFIRST
+          (tclTHEN (doN l2r c m) (apply_special_clear_request clear_flag c)) (loop l)
   in loop l
 
 let rewriteLR = general_rewrite true AllOccurrences true true
@@ -963,7 +976,7 @@ let discrEverywhere with_evars =
 *)
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
-  | Some c -> onInductionArg (discr with_evars) c
+  | Some c -> onInductionArg (fun clear_flag -> discr with_evars) c
 
 let discrConcl = discrClause false onConcl
 let discrHyp id = discrClause false (onHyp id)
@@ -1296,13 +1309,15 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
       inject_at_positions env sigma l2r u eq_clause posns
 	(tac (clenv_value eq_clause))
 
-let postInjEqTac ipats c n =
+let use_clear_hyp_by_default () = false
+
+let postInjEqTac clear_flag ipats c n =
   match ipats with
   | Some ipats ->
       let clear_tac =
-        if use_injection_pattern_l2r_order () && isVar c
-        then tclTRY (clear [destVar c])
-        else tclIDTAC in
+        let dft =
+          use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in
+        tclTRY (apply_clear_request clear_flag dft c) in
       let intro_tac =
         if use_injection_pattern_l2r_order ()
         then intros_pattern_bound n MoveLast ipats
@@ -1310,20 +1325,20 @@ let postInjEqTac ipats c n =
       tclTHEN clear_tac intro_tac
   | None -> tclIDTAC
 
-let injEq ipats =
+let injEq clear_flag ipats =
   let l2r =
     if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
   in
-  injEqThen (fun c i -> postInjEqTac ipats c i) l2r
+  injEqThen (fun c i -> postInjEqTac clear_flag ipats c i) l2r
 
-let inj ipats with_evars = onEquality with_evars (injEq ipats)
+let inj ipats with_evars clear_flag = onEquality with_evars (injEq clear_flag ipats)
 
 let injClause ipats with_evars = function
-  | None -> onNegatedEquality with_evars (injEq ipats)
+  | None -> onNegatedEquality with_evars (injEq None ipats)
   | Some c -> onInductionArg (inj ipats with_evars) c
 
 let injConcl = injClause None false None
-let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
+let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter begin fun gl ->
@@ -1341,10 +1356,12 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   end
 
 let dEqThen with_evars ntac = function
-  | None -> onNegatedEquality with_evars (decompEqThen ntac)
-  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
+  | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
+  | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c
 
-let dEq with_evars = dEqThen with_evars (fun c x -> Proofview.tclUNIT ())
+let dEq with_evars =
+  dEqThen with_evars (fun clear_flag c x ->
+    (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decompe_eq tac data cl =
   Proofview.Goal.raw_enter begin fun gl ->
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 82e30b940..2993c8d3a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -64,7 +64,7 @@ type delayed_open_constr_with_bindings =
     env -> evar_map -> evar_map * constr with_bindings
 
 val general_multi_multi_rewrite :
-  evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list ->
+  evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
     clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic
@@ -78,14 +78,14 @@ val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
   constr with_bindings induction_arg option -> unit Proofview.tactic
 val inj          : intro_pattern_expr Loc.located list option -> evars_flag ->
-  constr with_bindings -> unit Proofview.tactic
+  clear_flag -> constr with_bindings -> unit Proofview.tactic
 val injClause    : intro_pattern_expr Loc.located list option -> evars_flag ->
   constr with_bindings induction_arg option -> unit Proofview.tactic
-val injHyp       : Id.t -> unit Proofview.tactic
+val injHyp       : clear_flag -> Id.t -> unit Proofview.tactic
 val injConcl     : unit Proofview.tactic
 
 val dEq : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic
+val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8cf1e531d..a7d95c5e8 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -65,8 +65,8 @@ TACTIC EXTEND replace_term
 END
 
 let induction_arg_of_quantified_hyp = function
-  | AnonHyp n -> ElimOnAnonHyp n
-  | NamedHyp id -> ElimOnIdent (Loc.ghost,id)
+  | AnonHyp n -> None,ElimOnAnonHyp n
+  | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id)
 
 (* Versions *_main must come first!! so that "1" is interpreted as a
    ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
@@ -74,7 +74,7 @@ let induction_arg_of_quantified_hyp = function
 
 let elimOnConstrWithHoles tac with_evars c =
   Tacticals.New.tclWITHHOLES with_evars (tac with_evars) 
-    c.sigma (Some (ElimOnConstr c.it))
+    c.sigma (Some (None,ElimOnConstr c.it))
 
 TACTIC EXTEND simplify_eq_main
 | [ "simplify_eq" constr_with_bindings(c) ] ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ee875ce27..36affb541 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -308,9 +308,11 @@ let projectAndApply thin id eqname names depids =
     | _ -> tac id
     end
   in
-  let deq_trailer id _ neqns =
+  let deq_trailer id clear_flag _ neqns =
     tclTHENLIST
-      [(if not (List.is_empty names) then clear [id] else tclIDTAC);
+      [apply_clear_request clear_flag
+          (not (List.is_empty names) || use_clear_hyp_by_default ())
+          (mkVar id);
        (tclMAP_i neqns (fun idopt ->
 	 tclTRY (tclTHEN
 	   (intro_move idopt MoveLast)
@@ -325,7 +327,7 @@ let projectAndApply thin id eqname names depids =
     (* and apply a trailer which again try to substitute *)
     (fun id ->
       dEqThen false (deq_trailer id)
-	(Some (ElimOnConstr (mkVar id,NoBindings))))
+	(Some (None,ElimOnConstr (mkVar id,NoBindings))))
     id
 
 let nLastDecls i tac =
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index e2f87062e..80711cf81 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -270,18 +270,21 @@ let intern_bindings ist = function
 let intern_constr_with_bindings ist (c,bl) =
   (intern_constr ist c, intern_bindings ist bl)
 
+let intern_constr_with_bindings_arg ist (clear,c) =
+  (clear,intern_constr_with_bindings ist c)
+
   (* TODO: catch ltac vars *)
 let intern_induction_arg ist = function
-  | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
-  | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent (loc,id) ->
+  | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
+  | clear,ElimOnAnonHyp n as x -> x
+  | clear,ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
 	match intern_constr ist (CRef (Ident (dloc,id), None)) with
-	| GVar (loc,id),_ -> ElimOnIdent (loc,id)
-	| c -> ElimOnConstr (c,NoBindings)
+	| GVar (loc,id),_ -> clear,ElimOnIdent (loc,id)
+	| c -> clear,ElimOnConstr (c,NoBindings)
       else
-	ElimOnIdent (loc,id)
+	clear,ElimOnIdent (loc,id)
 
 let short_name = function
   | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
@@ -371,8 +374,8 @@ let intern_red_expr ist = function
   | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
 
-let intern_in_hyp_as ist lf (id,ipat) =
-  (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
+let intern_in_hyp_as ist lf (clear,id,ipat) =
+  (clear,intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
 
 let intern_hyp_list ist = List.map (intern_hyp ist)
 
@@ -459,12 +462,12 @@ let rec intern_atomic lf ist x =
                     intern_move_location ist hto)
   | TacExact c -> TacExact (intern_constr ist c)
   | TacApply (a,ev,cb,inhyp) ->
-      TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
+      TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
                 Option.map (intern_in_hyp_as ist lf) inhyp)
   | TacElim (ev,cb,cbo) ->
-      TacElim (ev,intern_constr_with_bindings ist cb,
+      TacElim (ev,intern_constr_with_bindings_arg ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)
-  | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
+  | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb)
   | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
@@ -555,7 +558,7 @@ let rec intern_atomic lf ist x =
   | TacRewrite (ev,l,cl,by) ->
       TacRewrite
 	(ev,
-	List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
+	List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings_arg ist c)) l,
 	clause_app (intern_hyp_location ist) cl,
 	Option.map (intern_pure_tactic ist) by)
   | TacInversion (inv,hyp) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b52a3e7e9..0432b08ec 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -768,8 +768,8 @@ and interp_intro_pattern_list_as_list ist env = function
 	List.map (interp_intro_pattern ist env) l)
   | l -> List.map (interp_intro_pattern ist env) l
 
-let interp_in_hyp_as ist env (id,ipat) =
-  (interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat)
+let interp_in_hyp_as ist env (clear,id,ipat) =
+  (clear,interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat)
 
 let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
@@ -812,11 +812,19 @@ let interp_constr_with_bindings ist env sigma (c,bl) =
   let sigma, c = interp_open_constr ist env sigma c in
   sigma, (c,bl)
 
+let interp_constr_with_bindings_arg ist env sigma (keep,c) =
+  let sigma, c = interp_constr_with_bindings ist env sigma c in
+  sigma, (keep,c)
+
 let interp_open_constr_with_bindings ist env sigma (c,bl) =
   let sigma, bl = interp_bindings ist env sigma bl in
   let sigma, c = interp_open_constr ist env sigma c in
   sigma, (c, bl)
 
+let interp_open_constr_with_bindings_arg ist env sigma (keep,c) =
+  let sigma, c = interp_open_constr_with_bindings ist env sigma c in
+  sigma,(keep,c)
+
 let loc_of_bindings = function
 | NoBindings -> Loc.ghost
 | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
@@ -829,22 +837,26 @@ let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
   let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
   sigma, (loc,cb)
 
+let interp_open_constr_with_bindings_arg_loc ist env sigma (keep,c) =
+  let sigma, c = interp_open_constr_with_bindings_loc ist env sigma c in
+  sigma,(keep,c)
+
 let interp_induction_arg ist gl arg =
   let env = pf_env gl and sigma = project gl in
   match arg with
-  | ElimOnConstr c ->
-      ElimOnConstr (interp_constr_with_bindings ist env sigma c)
-  | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent (loc,id) ->
+  | keep,ElimOnConstr c ->
+      keep,ElimOnConstr (interp_constr_with_bindings ist env sigma c)
+  | keep,ElimOnAnonHyp n as x -> x
+  | keep,ElimOnIdent (loc,id) ->
       let error () = user_err_loc (loc, "",
         strbrk "Cannot coerce " ++ pr_id id ++
         strbrk " neither to a quantified hypothesis nor to a term.")
       in
       let try_cast_id id' =
         if Tactics.is_quantified_hypothesis id' gl
-        then ElimOnIdent (loc,id')
+        then keep,ElimOnIdent (loc,id')
         else
-          (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
+          (try keep,ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
           with Not_found ->
             user_err_loc (loc,"",
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
@@ -862,18 +874,18 @@ let interp_induction_arg ist gl arg =
           let id = out_gen (topwit wit_var) v in
           try_cast_id id
         else if has_type v (topwit wit_int) then
-          ElimOnAnonHyp (out_gen (topwit wit_int) v)
+          keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
         else match Value.to_constr v with
         | None -> error ()
-        | Some c -> ElimOnConstr (sigma,(c,NoBindings))
+        | Some c -> keep,ElimOnConstr (sigma,(c,NoBindings))
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
-          ElimOnIdent (loc,id)
+          keep,ElimOnIdent (loc,id)
 	else
           let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in
           let (sigma,c) = interp_constr ist env sigma c in
-          ElimOnConstr (sigma,(c,NoBindings))
+          keep,ElimOnConstr (sigma,(c,NoBindings))
 
 (* Associates variables with values and gives the remaining variables and
    values *)
@@ -1544,7 +1556,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, l =
-          List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
+          List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
         in
         let tac = match cl with
           | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
@@ -1552,25 +1564,25 @@ and interp_atomic ist tac : unit Proofview.tactic =
               (fun l ->
                 Proofview.Goal.raw_enter begin fun gl ->
                   let env = Proofview.Goal.env gl in
-                  let (id,cl) = interp_in_hyp_as ist env cl in
-                  Tactics.apply_in a ev id l cl
+                  let (clear,id,cl) = interp_in_hyp_as ist env cl in
+                  Tactics.apply_in a ev clear id l cl
                 end) in
         Tacticals.New.tclWITHHOLES ev tac sigma l
       end
-  | TacElim (ev,cb,cbo) ->
+  | TacElim (ev,(keep,cb),cbo) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in 
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-        Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
+        Tacticals.New.tclWITHHOLES ev (Tactics.elim ev keep cb) sigma cbo
       end
-  | TacCase (ev,cb) ->
+  | TacCase (ev,(keep,cb)) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-        Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb
+        Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev keep) sigma cb
       end
   | TacFix (idopt,n) ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -1824,9 +1836,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
       Proofview.Goal.raw_enter begin fun gl ->
-        let l = List.map (fun (b,m,c) ->
+        let l = List.map (fun (b,m,(keep,c)) ->
           let f env sigma = interp_open_constr_with_bindings ist env sigma c in
-	  (b,m,f)) l in
+	  (b,m,keep,f)) l in
         let env = Proofview.Goal.env gl in
         let cl = interp_clause ist env cl in
         Equality.general_multi_multi_rewrite ev l cl
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 428061463..0ff4fe9b8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -44,10 +44,13 @@ let subst_bindings subst = function
 let subst_glob_with_bindings subst (c,bl) =
   (subst_glob_constr subst c, subst_bindings subst bl)
 
+let subst_glob_with_bindings_arg subst (clear,c) =
+  (clear,subst_glob_with_bindings subst c)
+
 let subst_induction_arg subst = function
-  | ElimOnConstr c -> ElimOnConstr (subst_glob_with_bindings subst c)
-  | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent id as x -> x
+  | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c)
+  | clear,ElimOnAnonHyp n as x -> x
+  | clear,ElimOnIdent id as x -> x
 
 let subst_and_short_name f (c,n) =
 (*  assert (n=None); *)(* since tacdef are strictly globalized *)
@@ -135,11 +138,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
   | TacExact c -> TacExact (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
-      TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
+      TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
   | TacElim (ev,cb,cbo) ->
-      TacElim (ev,subst_glob_with_bindings subst cb,
+      TacElim (ev,subst_glob_with_bindings_arg subst cb,
                Option.map (subst_glob_with_bindings subst) cbo)
-  | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
+  | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb)
   | TacFix (idopt,n) as x -> x
   | TacMutualFix (id,n,l) ->
       TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
@@ -194,7 +197,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacRewrite (ev,l,cl,by) ->
       TacRewrite (ev,
 		  List.map (fun (b,m,c) ->
-			      b,m,subst_glob_with_bindings subst c) l,
+			      b,m,subst_glob_with_bindings_arg subst c) l,
 		 cl,Option.map (subst_tactic subst) by)
   | TacInversion (DepInversion (k,c,l),hyp) ->
      TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb6894fef..2de4e26f3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -99,6 +99,19 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> apply_solve_class_goals:=a);
 }
 
+let clear_hyp_by_default = ref false
+
+let use_clear_hyp_by_default () = !clear_hyp_by_default
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "default clearing of hypotheses after use";
+      optkey   = ["Default";"Clearing";"Used";"Hypotheses"];
+      optread  = (fun () -> !clear_hyp_by_default) ;
+      optwrite = (fun b -> clear_hyp_by_default := b) }
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -159,6 +172,16 @@ let thin l gl =
   with Evarutil.ClearDependencyError (id,err) ->
     error_clear_dependency (pf_env gl) id err
 
+let apply_clear_request clear_flag dft c =
+  let check_isvar c =
+    if not (isVar c) then
+      error "keep/clear modifiers apply only to hypothesis names." in
+  let clear = match clear_flag with
+    | None -> dft && isVar c
+    | Some clear -> check_isvar c; clear in
+  if clear then Proofview.V82.tactic (thin [destVar c])
+  else Tacticals.New.tclIDTAC
+
 let internal_cut_gen b d t gl =
   try internal_cut b d t gl
   with Evarutil.ClearDependencyError (id,err) ->
@@ -167,8 +190,8 @@ let internal_cut_gen b d t gl =
 let internal_cut = internal_cut_gen false
 let internal_cut_replace = internal_cut_gen true
 
-let internal_cut_rev_gen b d t gl =
-  try internal_cut_rev b d t gl
+let internal_cut_rev_gen b id t gl =
+  try internal_cut_rev b id t gl
   with Evarutil.ClearDependencyError (id,err) ->
     error_clear_dependency (pf_env gl) id err
 
@@ -678,31 +701,36 @@ let rec intros_move = function
    or a term with bindings *)
 
 let onOpenInductionArg tac = function
-  | ElimOnConstr cbl ->
-      tac cbl
-  | ElimOnAnonHyp n ->
+  | clear_flag,ElimOnConstr cbl ->
+      tac clear_flag cbl
+  | clear_flag,ElimOnAnonHyp n ->
       Tacticals.New.tclTHEN
         (intros_until_n n)
-        (Tacticals.New.onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings))))
-  | ElimOnIdent (_,id) ->
+        (Tacticals.New.onLastHyp
+           (fun c -> tac clear_flag (Evd.empty,(c,NoBindings))))
+  | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
       Tacticals.New.tclTHEN
         (try_intros_until_id_check id)
-        (tac (Evd.empty,(mkVar id,NoBindings)))
+        (tac clear_flag (Evd.empty,(mkVar id,NoBindings)))
 
 let onInductionArg tac = function
-  | ElimOnConstr cbl ->
-      tac cbl
-  | ElimOnAnonHyp n ->
-      Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac (c,NoBindings)))
-  | ElimOnIdent (_,id) ->
+  | clear_flag,ElimOnConstr cbl ->
+      tac clear_flag cbl
+  | clear_flag,ElimOnAnonHyp n ->
+      Tacticals.New.tclTHEN
+        (intros_until_n n)
+        (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings)))
+  | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
-      Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings))
+      Tacticals.New.tclTHEN
+        (try_intros_until_id_check id)
+        (tac clear_flag (mkVar id,NoBindings))
 
 let map_induction_arg f = function
-  | ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl)
-  | ElimOnAnonHyp n -> ElimOnAnonHyp n
-  | ElimOnIdent id -> ElimOnIdent id
+  | clear_flag,ElimOnConstr (sigma,(c,bl)) -> clear_flag,ElimOnConstr (f (sigma,c),bl)
+  | clear_flag,ElimOnAnonHyp n as x -> x
+  | clear_flag,ElimOnIdent id as x -> x
 
 (**************************)
 (*     Cut tactics        *)
@@ -782,13 +810,19 @@ let check_unresolved_evars_of_metas clenv =
   | _ -> ())
   (meta_list clenv.evd)
 
+let clear_of_flag flag =
+  match flag with
+  | None -> true (* default for apply in *)
+  | Some b -> b
+
 (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
    goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last
    ones (resp [n] first ones if [sidecond_first] is [true]) being the
    [Ti] and the first one (resp last one) being [G] whose hypothesis
    [id] is replaced by P using the proof given by [tac] *)
 
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl =
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clear_flag id clenv gl =
+  let with_clear = clear_of_flag clear_flag in
   let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
   let clenv =
     if with_classes then
@@ -800,10 +834,15 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c
   if not with_evars && occur_meta new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
+  let id' = if with_clear then id else fresh_id [] id gl in
+  let exact_tac = refine_no_check new_hyp_prf in
   tclTHEN
     (tclEVARS clenv.evd)
-    ((if sidecond_first then assert_replacing else cut_replacing)
-      id new_hyp_typ (refine_no_check new_hyp_prf)) gl
+    (if sidecond_first then
+       tclTHENFIRST (internal_cut_gen with_clear id' new_hyp_typ) exact_tac
+     else
+       tclTHENLAST (internal_cut_rev_gen with_clear id' new_hyp_typ) exact_tac)
+    gl
 
 (********************************************)
 (*       Elimination tactics                *)
@@ -900,16 +939,20 @@ let general_elim_clause_gen elimtac indclause elim gl =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
   elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl
 
-let general_elim with_evars (c, lbindc) elim gl =
+let general_elim with_evars clear_flag (c, lbindc) elim gl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
   let indclause  = pf_apply make_clenv_binding gl (c, t) lbindc in
-  general_elim_clause_gen elimtac indclause elim gl
+  tclTHEN
+    (general_elim_clause_gen elimtac indclause elim)
+    (Proofview.V82.of_tactic
+       (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
+    gl
 
 (* Case analysis tactics *)
 
-let general_case_analysis_in_context with_evars (c,lbindc) gl =
+let general_case_analysis_in_context with_evars clear_flag (c,lbindc) gl =
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sort = elimination_sort_of_goal gl in
   let sigma, elim =
@@ -918,19 +961,21 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl =
     else
       pf_apply build_case_analysis_scheme_default gl mind sort in
   tclTHEN (tclEVARS sigma)
-  (general_elim with_evars (c,lbindc)
+  (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
     elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl
 
-let general_case_analysis with_evars (c,lbindc as cx) =
+let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
   match kind_of_term c with
     | Var id when lbindc == NoBindings ->
 	Tacticals.New.tclTHEN (try_intros_until_id_check id)
-	  (Proofview.V82.tactic (general_case_analysis_in_context with_evars cx))
+	  (Proofview.V82.tactic
+             (general_case_analysis_in_context with_evars clear_flag cx))
     | _ ->
-	Proofview.V82.tactic (general_case_analysis_in_context with_evars cx)
+	Proofview.V82.tactic
+          (general_case_analysis_in_context with_evars clear_flag cx)
 
-let simplest_case c = general_case_analysis false (c,NoBindings)
+let simplest_case c = general_case_analysis false None (c,NoBindings)
 
 (* Elimination tactic with bindings but using the default elimination
  * constant associated with the type. *)
@@ -951,39 +996,39 @@ let find_eliminator c gl =
     evd, {elimindex = None; elimbody = (c,NoBindings);
           elimrename = Some (true, constructors_nrealdecls ind)}
 
-let default_elim with_evars (c,_ as cx) =
+let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
     (Proofview.Goal.raw_enter begin fun gl ->
       let evd, elim = find_eliminator c gl in
 	Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
-	  (Proofview.V82.tactic (general_elim with_evars cx elim))
+	  (Proofview.V82.tactic (general_elim with_evars clear_flag cx elim))
     end)
     begin function
       | IsRecord ->
           (* For records, induction principles aren't there by default
              anymore.  Instead, we do a case analysis instead. *)
-          general_case_analysis with_evars cx
+          general_case_analysis with_evars clear_flag cx
       | e -> Proofview.tclZERO e
     end
 
-let elim_in_context with_evars c = function
+let elim_in_context with_evars clear_flag c = function
   | Some elim ->
       Proofview.V82.tactic
-        (general_elim with_evars c {elimindex = Some (-1); elimbody = elim;
+        (general_elim with_evars clear_flag c {elimindex = Some (-1); elimbody = elim;
                                     elimrename = None})
-  | None -> default_elim with_evars c
+  | None -> default_elim with_evars clear_flag c
 
-let elim with_evars (c,lbindc as cx) elim =
+let elim with_evars clear_flag (c,lbindc as cx) elim =
   match kind_of_term c with
     | Var id when lbindc == NoBindings ->
 	Tacticals.New.tclTHEN (try_intros_until_id_check id)
-	  (elim_in_context with_evars cx elim)
+	  (elim_in_context with_evars clear_flag cx elim)
     | _ ->
-	elim_in_context with_evars cx elim
+	elim_in_context with_evars clear_flag cx elim
 
 (* The simplest elimination tactic, with no substitutions at all. *)
 
-let simplest_elim c = default_elim false (c,NoBindings)
+let simplest_elim c = default_elim false None (c,NoBindings)
 
 (* Elimination in hypothesis *)
 (* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
@@ -1019,7 +1064,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
-  clenv_refine_in with_evars id elimclause'' gl
+  clenv_refine_in with_evars None id elimclause'' gl
 
 let general_elim_clause with_evars flags id c e =
   let elim = match id with
@@ -1117,7 +1162,7 @@ let solve_remaining_apply_goals gl =
     with Not_found -> tclIDTAC gl
   else tclIDTAC gl
     
-let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
+let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) gl0 =
   let flags =
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   (* The actual type of the theorem. It will be matched against the
@@ -1153,21 +1198,26 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
 		Loc.raise loc exn
 	in try_red_apply thm_ty0
   in
-    tclTHEN (try_main_apply with_destruct c) solve_remaining_apply_goals gl0
+    tclTHENLIST [
+      try_main_apply with_destruct c;
+      solve_remaining_apply_goals;
+      Proofview.V82.of_tactic
+        (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
+    ] gl0
 
 let rec apply_with_bindings_gen b e = function
   | [] -> tclIDTAC
-  | [cb] -> general_apply b b e cb
-  | cb::cbl ->
-      tclTHENLAST (general_apply b b e cb) (apply_with_bindings_gen b e cbl)
+  | [k,cb] -> general_apply b b e k cb
+  | (k,cb)::cbl ->
+      tclTHENLAST (general_apply b b e k cb) (apply_with_bindings_gen b e cbl)
 
-let apply_with_bindings cb = apply_with_bindings_gen false false [dloc,cb]
+let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
 
-let eapply_with_bindings cb = apply_with_bindings_gen false true [dloc,cb]
+let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)]
 
-let apply c = apply_with_bindings_gen false false [dloc,(c,NoBindings)]
+let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))]
 
-let eapply c = apply_with_bindings_gen false true [dloc,(c,NoBindings)]
+let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))]
 
 let apply_list = function
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -1212,15 +1262,19 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
   in
   aux (pf_apply make_clenv_binding gl (d,thm) lbind)
 
-let apply_in_once sidecond_first with_delta with_destruct with_evars id
-  (loc,(d,lbind)) gl0 =
+let apply_in_once sidecond_first with_delta with_destruct with_evars hyp_clear_flag
+    id (clear_flag,(loc,(d,lbind))) gl0 =
   let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
   let t' = pf_get_hyp_typ gl0 id in
   let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
   let rec aux with_destruct c gl =
     try
       let clause = apply_in_once_main flags innerclause (c,lbind) gl in
-      clenv_refine_in ~sidecond_first with_evars id clause gl
+      tclTHEN
+        (clenv_refine_in ~sidecond_first with_evars hyp_clear_flag id clause)
+        (Proofview.V82.of_tactic
+           (apply_clear_request clear_flag false c))
+        gl
     with e when with_destruct ->
       let e = Errors.push e in
       descend_in_conjunctions aux (fun _ -> raise e) c gl
@@ -1435,7 +1489,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
 	(Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in
       let cons = mkConstructU cons in
 	
-      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
+      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars None (dloc,(cons,lbind))) in
 	(Tacticals.New.tclTHENLIST
            [Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
   end
@@ -1770,23 +1824,23 @@ let tclMAPFIRST tacfun l =
   List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
 
 let general_apply_in sidecond_first with_delta with_destruct with_evars
-    id lemmas ipat =
+    with_clear id lemmas ipat =
   if sidecond_first then
     (* Skip the side conditions of the applied lemma *)
     Tacticals.New.tclTHENLAST
       (tclMAPLAST
-	(apply_in_once sidecond_first with_delta with_destruct with_evars id)
+	(apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
 	lemmas)
       (as_tac id ipat)
   else
     Tacticals.New.tclTHENFIRST
       (tclMAPFIRST
-	(apply_in_once sidecond_first with_delta with_destruct with_evars id)
+	(apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
 	lemmas)
       (as_tac id ipat)
 
-let apply_in simple with_evars id lemmas ipat =
-  general_apply_in false simple simple with_evars id lemmas ipat
+let apply_in simple with_evars clear_flag id lemmas ipat =
+  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
 
 (*****************************)
 (* Tactics abstracting terms *)
@@ -3283,7 +3337,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
   elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl
 
-let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
+let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps =
   Proofview.Goal.enter begin fun gl ->
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
@@ -3295,18 +3349,19 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
     induction_tac with_evars elim (hyp0,lbind) typ0;
     tclTRY (unfold_body hyp0);
-    thin [hyp0]
+    Proofview.V82.of_tactic
+      (apply_clear_request clear_flag true (mkVar hyp0))
   ]) in
   apply_induction_in_context
     (Some (hyp0,inhyps)) elim indvars names induct_tac
   end
 
-let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
+let induction_with_atomization_of_ind_arg clear_flag isrec with_evars elim names (hyp0,lbind) inhyps =
   Proofview.Goal.enter begin fun gl ->
   let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
   Tacticals.New.tclTHENLIST
     [Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0);
-    (induction_from_context isrec with_evars elim_info
+    (induction_from_context clear_flag isrec with_evars elim_info
       (hyp0,lbind) names inhyps)]
   end
 
@@ -3358,7 +3413,7 @@ let clear_unselected_context id inhyps cls gl =
 	  thin ids gl
       | None -> tclIDTAC gl
 
-let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
+let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
   let inhyps = match cls with
   | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
   | _ -> [] in
@@ -3369,7 +3424,7 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	Tacticals.New.tclTHEN
           (Proofview.V82.tactic (clear_unselected_context id inhyps cls))
 	  (induction_with_atomization_of_ind_arg
-	    isrec with_evars elim names (id,lbind) inhyps)
+	    clear_flag isrec with_evars elim names (id,lbind) inhyps)
     | _        ->
         Proofview.Goal.raw_enter begin fun gl ->
           let env = Proofview.Goal.env gl in
@@ -3385,7 +3440,8 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	      (letin_tac_gen with_eq
                  (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None)
 	      (induction_with_atomization_of_ind_arg
-	         isrec with_evars elim names (id,lbind) inhyps)
+	         (Some true)
+                 isrec with_evars elim names (id,lbind) inhyps)
           end
         end
 
@@ -3447,7 +3503,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
   if Int.equal (List.length lc) 1 && not ifi then
     (* standard induction *)
     onOpenInductionArg
-      (fun c -> induction_gen isrec with_evars elim names c cls)
+      (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim names c cls)
       (List.hd lc)
   else begin
     (* functional induction *)
@@ -3467,7 +3523,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
       (* Hook to recover standard induction on non-standard induction schemes *)
       (* will be removable when is_functional_induction will be more clever *)
       onInductionArg
-	(fun (c,lbind) ->
+	(fun _clear_flag (c,lbind) ->
 	  if lbind != NoBindings then
 	    error "'with' clause not supported here.";
 	  induction_gen_l isrec with_evars elim names [c]) (List.hd lc)
@@ -3475,7 +3531,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
       let newlc =
 	List.map (fun x ->
 	  match x with (* FIXME: should we deal with ElimOnIdent? *)
-	  | ElimOnConstr (x,NoBindings) -> x
+	  | _clear_flag,ElimOnConstr (x,NoBindings) -> x
 	  | _ -> error "Don't know where to find some argument.")
 	  lc in
       induction_gen_l isrec with_evars elim names newlc
@@ -3910,10 +3966,15 @@ module Simple = struct
     generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
                         cl)
 
-  let apply c = apply_with_bindings_gen false false [Loc.ghost,(c,NoBindings)]
-  let eapply c = apply_with_bindings_gen false true [Loc.ghost,(c,NoBindings)]
-  let elim c   = elim false (c,NoBindings) None
-  let case   c = general_case_analysis false (c,NoBindings)
+  let apply c =
+    apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
+  let eapply c =
+    apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))]
+  let elim c   = elim false None (c,NoBindings) None
+  let case   c = general_case_analysis false None (c,NoBindings)
+
+  let apply_in id c =
+    apply_in false false None id [None,(Loc.ghost, (c, NoBindings))] None
 
 end
 
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
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 9b4c62f87..1e8fad98e 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -169,5 +169,4 @@ Section Acc_generator.
     end.
 
 
-End Acc_generator. 
- 
\ No newline at end of file
+End Acc_generator.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0fbf0654f..15b370b06 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -79,12 +79,12 @@ let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c =
   induction false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+    [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 let destruct_on_using c id =
   destruct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+    [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None
     (None,Some (dl,IntroOrAndPattern [
                                     [dl,IntroAnonymous];
@@ -93,7 +93,7 @@ let destruct_on_using c id =
 
 let destruct_on c =
   destruct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+    [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 (* reconstruct the inductive with the correct deBruijn indexes *)
@@ -589,10 +589,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
                     Tacticals.New.tclREPEAT (
                       Tacticals.New.tclTHENLIST [
-                         apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None;
+                         Simple.apply_in freshz (andb_prop());
                          Proofview.Goal.enter begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
-                            (destruct false [Tacexpr.ElimOnConstr
+                            (destruct false [None,Tacexpr.ElimOnConstr
                                       (Evd.empty,((mkVar freshz,NoBindings)))]
                                   None
                                   (None, Some (dl,IntroOrAndPattern [[
@@ -723,7 +723,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                      Tacticals.New.tclTRY (
                       Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj None false (mkVar freshz,NoBindings);
+                     Equality.inj None false None (mkVar freshz,NoBindings);
 		     intros; (Proofview.V82.tactic simpl_in_concl);
                      Auto.default_auto;
                      Tacticals.New.tclREPEAT (