Fix erasure_live_test

MetaCoq · Aug 23, 2024 · c8e1658 · c8e1658
1 parent 4676c47
commit c8e1658
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v
@@ -83,10 +83,6 @@ Definition testmemo := Eval lazy in test memo.
 (** Cofix *)
 From Coq Require Import StreamMemo.
 
-MetaCoq Quote Recursively Definition memo := memo_make.
-
-Definition testmemo := Eval lazy in test memo.
-
 (** Ackermann **)
 Fixpoint ack (n m:nat) {struct n} : nat :=
   match n with