diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-20 08:15:06 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-20 08:15:06 +0000 |
| commit | e7fc963667a6cfbf9f8516f49ea1dcb9d6779f2d (patch) | |
| tree | 9ed81297689fdbf697d25e8fba324e9aee848bf1 /test-suite/complexity | |
| parent | 2a4d714a146645570f667c5e5cf9b82c42886296 (diff) | |
fixed guard check with commutative cuts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/guard.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v index 387263e2f..ceb7835a6 100644 --- a/test-suite/complexity/guard.v +++ b/test-suite/complexity/guard.v @@ -1,4 +1,4 @@ -(* Examples to check that the guard condition does not unfold +(* Examples to check that the guard condition does not evaluate irrelevant subterms *) (* Expected time < 1.00s *) Require Import Bool. @@ -15,3 +15,16 @@ Timeout 5 Time Fixpoint F n := | S k => if slow 100 then F k else 0 end. + +Fixpoint slow2 n := + match n with + | 0 => 0 + | S k => slow2 k + slow2 k + end. + +Timeout 5 Time Fixpoint F' n := + match n with + | 0 => 0 + | S k => + if slow2 100 then F' k else 0 + end. |