Fix test suite

MetaCoq · Oct 3, 2023 · 357e8a7 · 357e8a7
1 parent f2b1cc0
commit 357e8a7
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v
@@ -323,8 +323,10 @@ Require Import Coq.Arith.Compare_dec.
 Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Arith.Peano_dec.
 Require Import Arith Init.Wf.
+Require Import Program.
 Program Fixpoint provedCopy (n:nat) {wf lt n} : nat :=
   match n with 0 => 0 | S k => S (provedCopy k) end.
+
 Print Assumptions provedCopy.
 (* MetaCoq Quote Recursively Definition pCopy := provedCopy. program *)