From 2d3d9d4c7a4276fbc6bdf553f082ac12a56824d3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Jun 2008 13:02:48 +0000
Subject: - 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
---
 test-suite/success/Discriminate.v | 23 +++++++++++++++++++++++
 test-suite/success/Injection.v    | 27 +++++++++++++++++++++++++--
 2 files changed, 48 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index f28c83deba..b57c547819 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 606e884aee..867d73746c 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.
 
- *)
+*)
-- 
cgit v1.2.3