- 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

1 files changed, 19 insertions, 14 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25e920976..c8f92b60f 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 ->