- 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

2 files changed, 48 insertions, 2 deletions

diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index f28c83deb..b57c54781 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -9,3 +9,26 @@ Qed.
 Lemma l2 : forall H : 0 = 1, H = H.   
  discriminate H.
 Qed.
+
+(* Check the variants of discriminate *)
+
+Goal O = S O -> True.
+discriminate 1.
+Undo.
+intros.
+discriminate H.
+Undo.
+Ltac g x := discriminate x.
+g H.
+Abort.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+try discriminate (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+ediscriminate (H O).
+instantiate (1:=O).
+Abort.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 606e884ae..867d73746 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -43,6 +43,29 @@ intros; injection H as Hyt Hxz.
 exact Hxz.
 Qed.
 
+(* Check the variants of injection *)
+
+Goal forall x y, S x = S y -> True.
+injection 1 as H'.
+Undo.
+intros.
+injection H as H'.
+Undo.
+Ltac f x := injection x.
+f H.
+Abort.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+try injection (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+einjection (H O).
+instantiate (1:=O).
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
@@ -53,7 +76,7 @@ Abort.
 
 *)
 
-(* Accept does not project on discriminable positions... allow it?
+(* Injection does not project on discriminable positions... allow it?
 
 Goal 1=2 -> 1=0.
 intro H.
@@ -61,4 +84,4 @@ injection H.
 intro; assumption.
 Qed.
 
- *)
+*)