diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index 97c5c67e3..e0e685240 100644 --- 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