Il ne doit plus y avoir de preuves non terminées à la sortie du fichier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index bac62f16e..e93be7763 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -20,3 +20,25 @@ Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a.
 Lemma lem2 : True.
 U.
 Qed.
+
+(* Check that Match giving non-tactic arguments are evaluated at Let-time *)
+ 
+Tactic Definition B :=
+ Let y = (Match Context With [ z:? |- ? ] -> z) In 
+ Intro H1; Exact y.
+
+Lemma lem3 : True -> False -> True -> False.
+Intros H H0.
+B.  (* y is H0 if at let-time, H1 otherwise *)
+Qed.
+
+(* Checks the matching order of hypotheses *)
+Tactic Definition Y := Match Context With [ x:?; y:? |- ? ] -> Apply x.
+Tactic Definition Z := Match Context With [ y:?; x:? |- ? ] -> Apply x.
+
+Lemma lem4 : (True->False) -> (False->False) -> False.
+Intros H H0.
+Z. (* Apply H0 *)
+Y. (* Apply H *)
+Exact I.
+Qed.