Skip to content

Commit c8e1658

Browse files
committed
Fix erasure_live_test
1 parent 4676c47 commit c8e1658

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

test-suite/erasure_live_test.v

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,10 +83,6 @@ Definition testmemo := Eval lazy in test memo.
8383
(** Cofix *)
8484
From Coq Require Import StreamMemo.
8585

86-
MetaCoq Quote Recursively Definition memo := memo_make.
87-
88-
Definition testmemo := Eval lazy in test memo.
89-
9086
(** Ackermann **)
9187
Fixpoint ack (n m:nat) {struct n} : nat :=
9288
match n with

0 commit comments

Comments
 (0)