diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-14 10:06:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-14 10:06:54 +0000 |
| commit | 100120634953b594169931409122c580fa12e5b1 (patch) | |
| tree | 02edb5c6ff8c0dd66737156a6bd2c991ff0b0493 /test-suite | |
| parent | b135398867bf04da57eac57df29e3136f8a0f14e (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2785 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltac.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 04d7c87c5..bac62f16e 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -9,6 +9,11 @@ f plus. Reflexivity. Qed. +(* Submitted by Pierre Crégut *) +(* Check syntactic correctness *) +Recursive Tactic Definition F x := Idtac; (G x) +And G y := Idtac; (F y). + (* Check that Match Context keeps a closure *) Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a. |