From c8e165840a0b90e78f1d3f9adb2fe11974ef95ad Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 23 Aug 2024 17:53:10 +0200 Subject: [PATCH] Fix erasure_live_test --- test-suite/erasure_live_test.v | 4 ---- 1 file changed, 4 deletions(-) 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