- Implantation de la suggestion 1873 sur discriminate. Au final,

  discriminate/injection/simplify_eq acceptent maintenant un terme
  comme argument. Les clauses "with" et les variantes "e" sont aussi
  acceptées. Aussi, discriminate sans argument essaie maintenant
  toutes les hyps quantifiées (au lieu de traiter seulement les buts
  t1<>t2).

--This line, and those below, will be ignored--

M    doc/refman/RefMan-tac.tex
M    CHANGES
M    pretyping/evd.ml
M    pretyping/termops.ml
M    pretyping/termops.mli
M    pretyping/clenv.ml
M    tactics/extratactics.ml4
M    tactics/inv.ml
M    tactics/equality.ml
M    tactics/tactics.mli
M    tactics/equality.mli
M    tactics/tacticals.ml
M    tactics/eqdecide.ml4
M    tactics/tacinterp.ml
M    tactics/tactics.ml
M    tactics/extratactics.mli
M    toplevel/auto_ind_decl.ml
M    contrib/funind/invfun.ml
M    test-suite/success/Discriminate.v
M    test-suite/success/Injection.v
M    proofs/clenvtac.mli
M    proofs/clenvtac.ml


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

10 files changed, 208 insertions, 105 deletions

diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 8aef9c50b2..61100f0a50 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -75,7 +75,7 @@ let mkBranches c1 c2 =
 let solveNoteqBranch side = 
   tclTHEN (choose_noteq side)
     (tclTHEN (intro_force true)
-      (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
+      (onLastHyp (fun id -> Extratactics.h_discrHyp id)))
 
 let h_solveNoteqBranch side =
   Refiner.abstract_extended_tactic "solveNoteqBranch" [] 
@@ -115,7 +115,7 @@ let diseqCase eqonleft =
   (tclTHEN  red_in_concl
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
-  (tclTHEN  (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
+  (tclTHEN  (Extratactics.h_injHyp absurd)
             (full_trivial [])))))))
 
 let solveArg eqonleft op a1 a2 tac g = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f907b1fd77..3bfc719e2c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,6 +40,9 @@ open Vernacexpr
 open Setoid_replace
 open Declarations
 open Indrec
+open Printer
+open Clenv
+open Clenvtac
 
 (* Rewriting tactics *)
 
@@ -550,66 +553,84 @@ exception NotDiscriminable
 
 let eq_baseid = id_of_string "e"
 
-let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort =
+let apply_on_clause (f,t) clause =
+  let sigma = Evd.evars_of clause.evd in
+  let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
+  let argmv = 
+    (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
+     | Meta mv -> mv
+     | _  -> errorlabstrm "" (str "Ill-formed clause applicator")) in
+  clenv_fchain argmv f_clause clause
+
+let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
+  let eqn = mkApp(lbeq.eq,[|t;t1;t2|]) in
   let discriminator =
     build_discriminator sigma e_env dirn (mkVar e) sort cpath in
   let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
-  tclCOMPLETE 
-    ((tclTHENS (cut_intro absurd_term)
-      [onLastHyp gen_absurdity; 
-       refine (mkApp (pf,[|mkVar id|]))]))
+  let pf_ty = mkArrow eqn absurd_term in
+  let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
+  tclTHENS (cut_intro absurd_term)
+    [onLastHyp gen_absurdity; res_pf absurd_clause]
 
-let discrEq (lbeq,(t,t1,t2) as u) id gls =
-  let sigma = project gls in
+let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
+  let sigma = Evd.evars_of eq_clause.evd in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inr _ ->
-	errorlabstrm "discr" (str" Not a discriminable equality")
+	errorlabstrm "discr" (str"Not a discriminable equality")
     | Inl (cpath, (_,dirn), _) ->
 	let sort = pf_apply get_type_of gls (pf_concl gls) in 
-	discr_positions env sigma u id cpath dirn sort gls
-
-let onEquality tac id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+	discr_positions env sigma u eq_clause cpath dirn sort gls
+
+let onEquality with_evars tac (c,lbindc) gls =
+  let t = pf_type_of gls c in
+  let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in
+  let eq_clause = make_clenv_binding gls (c,t') lbindc in
+  let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
+  let eqn = clenv_type eq_clause' in
   let eq =
     try find_eq_data_decompose eqn
     with PatternMatchingFailure ->
-      errorlabstrm "" (pr_id id ++ str": not a primitive equality") 
-  in tac eq id gls
+      errorlabstrm "" (str"No primitive equality found") in
+  tclTHEN
+    (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) 
+    (tac eq eq_clause') gls
 
-let onNegatedEquality tac gls =
+let onNegatedEquality with_evars tac gls =
   let ccl = pf_concl gls in
-  let eq =
-    try match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
-      | Prod (_,t,u) when is_empty_type u ->
-          find_eq_data_decompose (pf_whd_betadeltaiota gls t)
-      | _ -> raise PatternMatchingFailure
-    with PatternMatchingFailure ->
+  match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
+  | Prod (_,t,u) when is_empty_type u ->
+      tclTHEN introf
+        (onLastHyp (fun id -> 
+          onEquality with_evars tac (mkVar id,NoBindings))) gls
+  | _ -> 
       errorlabstrm "" (str "Not a negated primitive equality")
-  in tclTHEN introf (onLastHyp (tac eq)) gls
 
-let discrSimpleClause = function
-  | None -> onNegatedEquality discrEq
-  | Some ((_,id),_) -> onEquality discrEq id
+let discrSimpleClause with_evars = function
+  | None -> onNegatedEquality with_evars discrEq
+  | Some ((_,id),_) -> onEquality with_evars discrEq (mkVar id,NoBindings)
 
-let discr = onEquality discrEq
+let discr with_evars = onEquality with_evars discrEq
 
-let discrClause = onClauses discrSimpleClause
+let discrClause with_evars = onClauses (discrSimpleClause with_evars)
 
-let discrEverywhere = 
+let discrEverywhere with_evars = 
   tclORELSE
-    (Tacticals.tryAllClauses discrSimpleClause)
+    (tclTHEN
+      (tclREPEAT introf) 
+      (Tacticals.tryAllHyps
+        (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
     (fun gls -> 
        errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
 
-let discr_tac = function
-  | None -> discrEverywhere
-  | Some id -> try_intros_until discr id
+let discr_tac with_evars = function
+  | None -> discrEverywhere with_evars
+  | Some c -> onInductionArg (discr with_evars) c
 
-let discrConcl gls  = discrClause onConcl gls
-let discrHyp id gls = discrClause (onHyp id) gls
+let discrConcl gls  = discrClause false onConcl gls
+let discrHyp id gls = discrClause false (onHyp id) gls
 
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
@@ -828,7 +849,7 @@ let simplify_args env sigma t =
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
+let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let injectors =
@@ -837,9 +858,12 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
         (* arbitrarily take t1' as the injector default value *)
 	let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
 	let injfun = mkNamedLambda e t injbody in
-	let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
-	let ty = simplify_args env sigma (get_type_of env sigma pf) in
-	  (pf,ty))
+	let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
+	let pf_typ = get_type_of env sigma pf in
+	let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
+        let pf = clenv_value_cast_meta inj_clause in
+	let ty = simplify_args env sigma (clenv_type inj_clause) in
+	(pf,ty))
       posns in
   if injectors = [] then
     errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
@@ -850,14 +874,13 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
 exception Not_dep_pair
 
 
-let injEq ipats (eq,(t,t1,t2)) id gls =
-  let sigma = project gls in
-  let env = pf_env gls in
+let injEq ipats (eq,(t,t1,t2)) eq_clause =
+  let sigma = Evd.evars_of eq_clause.evd in
+  let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
     | Inl _ ->
 	errorlabstrm "Inj"
-	  (str (string_of_id id) ++
-	    str" is not a projectable equality but a discriminable one")
+	  (str"Not a projectable equality but a discriminable one")
     | Inr [] ->
 	errorlabstrm "Equality.inj" 
 	   (str"Nothing to do, it is an equality between convertible terms")
@@ -895,45 +918,44 @@ let injEq ipats (eq,(t,t1,t2)) id gls =
                         [|ar1.(0);Ind_tables.find_eq_dec_proof ind;
                           ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
                   )) (Auto.trivial [] [])
-                ] gls
+                ]
 (* not a dep eq or no decidable type found *)
             ) else (raise Not_dep_pair) 
-        ) with _ -> (
-	tclTHEN 
-	  (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
+        ) with _ ->
+	tclTHEN
+	  (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns)
 	  (intros_pattern None ipats)
-	  gls
-        )
 
-let inj ipats = onEquality (injEq ipats)
+let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
-let injClause ipats = function
-  | None -> onNegatedEquality (injEq ipats)
-  | Some id -> try_intros_until (inj ipats) id
+let injClause ipats with_evars = function
+  | None -> onNegatedEquality with_evars (injEq ipats)
+  | Some c -> onInductionArg (inj ipats with_evars) c
 
-let injConcl gls  = injClause [] None gls
-let injHyp id gls = injClause [] (Some id) gls
+let injConcl gls  = injClause [] false None gls
+let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
 
-let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls =
+let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in 
-  let sigma = project gls in
+  let sigma = Evd.evars_of clause.evd in
   let env = pf_env gls in 
   match find_positions env sigma t1 t2 with
     | Inl (cpath, (_,dirn), _) ->
-	discr_positions env sigma u id cpath dirn sort gls
+	discr_positions env sigma u clause cpath dirn sort gls
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
         ntac 0 gls
     | Inr posns ->
 	tclTHEN
-	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns))
+	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause
+	    (List.rev posns))
 	  (ntac (List.length posns))
 	  gls
 
-let dEqThen ntac = function
-  | None -> onNegatedEquality (decompEqThen ntac)
-  | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id
+let dEqThen with_evars ntac = function
+  | None -> onNegatedEquality with_evars (decompEqThen ntac)
+  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
 
-let dEq = dEqThen (fun x -> tclIDTAC)
+let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
 
 let rewrite_msg = function 
   | None -> str "passed term is not a primitive equality" 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index acbaca235e..3c7f9c6b0c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -67,18 +67,22 @@ val replace_in : identifier -> constr -> constr -> tactic
 val replace_by : constr -> constr -> tactic -> tactic
 val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
 
-val discr        : identifier -> tactic
+val discr        : evars_flag -> constr with_ebindings -> tactic
 val discrConcl   : tactic
-val discrClause  : clause -> tactic
+val discrClause  : evars_flag -> clause -> tactic
 val discrHyp     : identifier -> tactic
-val discrEverywhere     : tactic
-val discr_tac    : quantified_hypothesis option -> tactic
-val inj          : intro_pattern_expr list -> identifier -> tactic
-val injClause    : intro_pattern_expr list -> quantified_hypothesis option ->
-                   tactic
-
-val dEq : quantified_hypothesis option -> tactic
-val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic
+val discrEverywhere : evars_flag -> tactic
+val discr_tac    : evars_flag -> 
+  constr with_ebindings induction_arg option -> tactic
+val inj          : intro_pattern_expr list -> evars_flag ->
+  constr with_ebindings -> tactic
+val injClause    : intro_pattern_expr list -> evars_flag -> 
+  constr with_ebindings induction_arg option -> tactic
+val injHyp       : identifier -> tactic
+val injConcl     : tactic
+
+val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic
+val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic
 
 val make_iterated_tuple : 
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index dd716024d5..5d374215de 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -16,6 +16,8 @@ open Genarg
 open Extraargs
 open Mod_subst
 open Names
+open Tacexpr
+open Rawterm
 
 (* Equality *)
 open Equality
@@ -41,25 +43,93 @@ TACTIC EXTEND replace_term
   -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
 END
 
+let induction_arg_of_quantified_hyp = function
+  | AnonHyp n -> ElimOnAnonHyp n
+  | NamedHyp id -> ElimOnIdent (Util.dummy_loc,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
+   ElimOnIdent and not as "constr" *)
+
+TACTIC EXTEND simplify_eq_main
+| [ "simplify_eq" constr_with_bindings(c) ] ->
+    [ dEq false (Some (ElimOnConstr c)) ]
+END
 TACTIC EXTEND simplify_eq
-  [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
+  [ "simplify_eq" ] -> [ dEq false None ]
+| [ "simplify_eq" quantified_hypothesis(h) ] ->
+    [ dEq false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND esimplify_eq_main
+| [ "esimplify_eq" constr_with_bindings(c) ] ->
+    [ dEq true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND esimplify_eq
+| [ "esimplify_eq" ] -> [ dEq true None ]
+| [ "esimplify_eq" quantified_hypothesis(h) ] ->
+    [ dEq true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
+TACTIC EXTEND discriminate_main
+| [ "discriminate" constr_with_bindings(c) ] ->
+    [ discr_tac false (Some (ElimOnConstr c)) ]
+END
 TACTIC EXTEND discriminate
-  [ "discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ]
+| [ "discriminate" ] -> [ discr_tac false None ]
+| [ "discriminate" quantified_hypothesis(h) ] ->
+    [ discr_tac false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND ediscriminate_main
+| [ "ediscriminate" constr_with_bindings(c) ] ->
+    [ discr_tac true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND ediscriminate
+| [ "ediscriminate" ] -> [ discr_tac true None ]
+| [ "ediscriminate" quantified_hypothesis(h) ] ->
+    [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-let h_discrHyp id = h_discriminate (Some id)
+let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings)
 
+TACTIC EXTEND injection_main
+| [ "injection" constr_with_bindings(c) ] ->
+    [ injClause [] false (Some (ElimOnConstr c)) ]
+END 
 TACTIC EXTEND injection
-  [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ]
+| [ "injection" ] -> [ injClause [] false None ]
+| [ "injection" quantified_hypothesis(h) ] -> 
+    [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND einjection_main
+| [ "einjection" constr_with_bindings(c) ] ->
+    [ injClause [] true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND einjection
+| [ "einjection" ] -> [ injClause [] true None ]
+| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ]
+END 
+TACTIC EXTEND injection_as_main
+| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat false (Some (ElimOnConstr c)) ]
 END 
 TACTIC EXTEND injection_as
-  [ "injection" quantified_hypothesis_opt(h) 
-    "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ]
+| [ "injection" "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat false None ]
+| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+    [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ]
+END 
+TACTIC EXTEND einjection_as_main
+| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat true (Some (ElimOnConstr c)) ]
+END 
+TACTIC EXTEND einjection_as
+| [ "einjection" "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat true None ]
+| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+    [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-let h_injHyp id = h_injection (Some id)
+let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
 
 TACTIC EXTEND conditional_rewrite
 | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 341716c01f..7a5314c367 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -9,10 +9,9 @@
 (*i $Id$ i*)
 
 open Proof_type
-open Rawterm
 
-val h_discrHyp : quantified_hypothesis -> tactic
-val h_injHyp : quantified_hypothesis -> tactic
+val h_discrHyp : Names.identifier -> tactic
+val h_injHyp : Names.identifier -> tactic
 
 val refine_tac : Evd.open_constr -> tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a77a979060..a25fa285b1 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -331,7 +331,7 @@ let projectAndApply thin id eqname names depids gls =
   substHypIfVariable
     (* If no immediate variable in the equation, try to decompose it *)
     (* and apply a trailer which again try to substitute *)
-    (fun id -> dEqThen (deq_trailer id) (Some (NamedHyp id)))
+    (fun id -> dEqThen false (deq_trailer id) (Some (ElimOnIdent (dummy_loc,id))))
     id
     gls
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 876f13c33d..897c8fd982 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1150,7 +1150,7 @@ let debugging_exception_step ist signal_anomaly e pp =
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ 
    str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ 
-   str "which cannot be coerced to " ++ str s)
+   strbrk "which cannot be coerced to " ++ str s)
 
 exception CannotCoerceTo of string
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 577ef0c6f2..3d5fd753ec 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -325,10 +325,6 @@ let elimination_sort_of_hyp id gl =
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
 
-let last_arg c = match kind_of_term c with
-  | App (f,cl) -> array_last cl
-  | _ -> anomaly "last_arg"
-
 let general_elim_then_using mk_elim 
   isrec allnames tac predicate (indbindings,elimbindings) 
   ind indclause gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25e9209761..c8f92b60f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -469,6 +469,21 @@ let rec intros_rmove = function
  		    move_to_rhyp destopt;
 		    intros_rmove rest ]
 
+(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+   or a term with bindings *)
+
+let onInductionArg tac = function
+  | ElimOnConstr (c,lbindc as cbl) -> 
+      if isVar c & lbindc = NoBindings then 
+	tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl)
+      else
+	tac cbl
+  | ElimOnAnonHyp n ->
+      tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> tac (c,NoBindings)))
+  | ElimOnIdent (_,id) ->
+      (*Identifier apart because id can be quantified in goal and not typable*)
+      tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings))
+
 (**************************)
 (*  Refinement tactics    *)
 (**************************)
@@ -2531,7 +2546,6 @@ let induct_destruct_l isrec with_evars lc elim names cls =
       "'in' clause not supported when several induction hypothesis are given";
   new_induct_gen_l isrec with_evars elim names newlc
 
-
 (* Induction either over a term, over a quantified premisse, or over
    several quantified premisses (like with functional induction
    principles). 
@@ -2540,19 +2554,10 @@ let induct_destruct_l isrec with_evars lc elim names cls =
 let induct_destruct isrec with_evars lc elim names cls =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
   if List.length lc = 1 then (* induction on one arg: use old mechanism *)
-    try 
-      let c = List.hd lc in
-      match c with
-	| ElimOnConstr c -> new_induct_gen isrec with_evars elim names c cls
-	| ElimOnAnonHyp n ->
-	    tclTHEN (intros_until_n n)
-	      (tclLAST_HYP (fun c -> 
-		new_induct_gen isrec with_evars elim names (c,NoBindings) cls))
-	      (* Identifier apart because id can be quantified in goal and not typable *)
-	| ElimOnIdent (_,id) ->
-	    tclTHEN (tclTRY (intros_until_id id))
-	      (new_induct_gen isrec with_evars elim names
-		(mkVar id,NoBindings) cls)
+    try
+      onInductionArg
+	(fun c -> new_induct_gen isrec with_evars elim names c cls)
+	(List.hd lc)
     with (* If this fails, try with new mechanism but if it fails too,
 	    then the exception is the first one. *)
       | x ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0492e296f2..700c25f6e8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -101,6 +101,13 @@ val intros_clearing      : bool list -> tactic
 val try_intros_until :
   (identifier -> tactic) -> quantified_hypothesis -> tactic
 
+(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+   or a term with bindings *)
+
+val onInductionArg : 
+  (constr with_ebindings -> tactic) ->
+    constr with_ebindings induction_arg -> tactic
+
 (*s Introduction tactics with eliminations. *)
 
 val intro_pattern     : identifier option -> intro_pattern_expr      -> tactic