diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-29 14:47:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-29 14:47:14 +0000 |
| commit | 736294486e4d5a4238c98af1ba35e20e59215ee2 (patch) | |
| tree | 900c0a057c9e9d06ad881bec3cc1013c00b351b0 /test-suite/output | |
| parent | 5a75a4d046c24a5c6c9e452f08f0fa8305c88226 (diff) | |
Oops... the trunk behaviour is different
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11296 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Fixpoint.out | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 8bc855216..09bc00886 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -14,10 +14,12 @@ fix even_pos_odd_pos 2 intros. destruct H. omega. + apply odd_pos_even_pos in H. omega. - intros. - destruct H. - apply even_pos_odd_pos in H. - omega. + intros. + destruct H. + apply even_pos_odd_pos in H. + omega. + |