diff options
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/constructor.v | 1 | ||||
| -rw-r--r-- | test-suite/complexity/f_equal.v | 1 | ||||
| -rw-r--r-- | test-suite/complexity/injection.v | 1 | ||||
| -rw-r--r-- | test-suite/complexity/ring.v | 1 | ||||
| -rw-r--r-- | test-suite/complexity/ring2.v | 1 | ||||
| -rw-r--r-- | test-suite/complexity/setoid_rewrite.v | 1 | ||||
| -rw-r--r-- | test-suite/complexity/unification.v | 1 |
7 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v index c5e1953829..31217ca75e 100644 --- a/test-suite/complexity/constructor.v +++ b/test-suite/complexity/constructor.v @@ -214,3 +214,4 @@ Fixpoint expand (n : nat) : Prop := Example Expand : expand 2500. Time constructor. (* ~0.45 secs *) +Qed. diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v index 86698fa872..c2c566930b 100644 --- a/test-suite/complexity/f_equal.v +++ b/test-suite/complexity/f_equal.v @@ -12,3 +12,4 @@ end. Goal stupid 23 = stupid 23. Timeout 5 Time f_equal. +Abort. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index a76fa19d3c..298a07c1c4 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -111,3 +111,4 @@ Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 -> Proof. intros. Timeout 10 Time injection H. +Abort. diff --git a/test-suite/complexity/ring.v b/test-suite/complexity/ring.v index 51f7c4dabc..2d585ce5c5 100644 --- a/test-suite/complexity/ring.v +++ b/test-suite/complexity/ring.v @@ -5,3 +5,4 @@ Require Import ZArith. Open Scope Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. +Abort. diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index 04fa59075b..1c119b8e42 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -50,3 +50,4 @@ Infix "+" := Zadd : Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. +Abort. diff --git a/test-suite/complexity/setoid_rewrite.v b/test-suite/complexity/setoid_rewrite.v index 2e3b006ef0..10b270ccad 100644 --- a/test-suite/complexity/setoid_rewrite.v +++ b/test-suite/complexity/setoid_rewrite.v @@ -8,3 +8,4 @@ Variable f : nat -> Prop. Goal forall U:Prop, f 100 <-> U. intros U. Timeout 5 Time setoid_replace U with False. +Abort. diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v index d2ea527516..0c9915c84e 100644 --- a/test-suite/complexity/unification.v +++ b/test-suite/complexity/unification.v @@ -49,3 +49,4 @@ Goal )))) . Timeout 2 Time try refine (refl_equal _). +Abort. |