- 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, 2 insertions, 2 deletions

diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 0160c290f..63d44916b 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -573,9 +573,9 @@ let rec reflexivity_with_destruct_cases g =
 	       match kind_of_term  (pf_type_of g (mkVar id)) with 
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> 
 		     if Equality.discriminable (pf_env g) (project g) t1 t2 
-		     then Equality.discr id g
+		     then Equality.discrHyp id g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite]  g
+		     then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )