From 357e8a7ddd140f4396c18eb9bd95e822f9363d25 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau <matthieu.sozeau@inria.fr> Date: Tue, 3 Oct 2023 11:27:01 +0200 Subject: [PATCH] Fix test suite --- test-suite/erasure_live_test.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index c619b7d5e..b3f89a2fb 100644 --- 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 *)