From 69f4580c239548082d899b3719b5de2d686252c3 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 12 Jun 2019 17:05:55 +0200 Subject: Removing the Admitted warning when running "make check-admitted" --- mppa_k1c/ExtValues.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 8e6aa028..3370fae3 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -424,7 +424,7 @@ Qed. (* Lemma signed_0_eqb : forall x, (Z.eqb (Int.signed x) 0) = Int.eq x Int.zero. -Admitted. +Qed. *) Lemma Z_quot_le: forall a b, -- cgit