Merge branch 'coq-8.20'

MetaCoq · Aug 23, 2024 · a08708b · a08708b
2 parents a40e807 + c8e1658
commit a08708b
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