- 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, 5 insertions, 4 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0ef8356892..9192db7222 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -525,7 +525,7 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                      intro_using freshz;
                      intros;
                      tclTRY ( 
-                      tclORELSE reflexivity (Equality.discr_tac None)
+                      tclORELSE reflexivity (Equality.discr_tac false None)
                      );
                      simpl_in_hyp
 		       ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
@@ -643,9 +643,10 @@ let compute_lb_tact ind lnamesparrec nparrec =
                      intro_using freshz;
                      intros;
                      tclTRY ( 
-                      tclORELSE reflexivity (Equality.discr_tac None)
+                      tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj [] freshz; intros; simpl_in_concl;
+                     Equality.inj [] false (mkVar freshz,Rawterm.NoBindings);
+		     intros; simpl_in_concl;
                      Auto.default_auto;
                      tclREPEAT (
                       tclTHENSEQ [apply (andb_true_intro());
@@ -806,6 +807,6 @@ let compute_dec_tact ind lnamesparrec nparrec =
                                 Rawterm.NoBindings
                               )
                               true);
-        Pfedit.by (Equality.discr_tac None)
+        Pfedit.by (Equality.discr_tac false None)