aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-06-12 17:05:55 +0200
committerCyril SIX <cyril.six@kalray.eu>2019-06-12 17:05:55 +0200
commit69f4580c239548082d899b3719b5de2d686252c3 (patch)
treeaea1e90e422eb21d42d0811bd600b1505ea1e90f
parent8f88967df89f625d1a15f4c36f49450fe42e97db (diff)
downloadcompcert-kvx-69f4580c239548082d899b3719b5de2d686252c3.tar.gz
compcert-kvx-69f4580c239548082d899b3719b5de2d686252c3.zip
Removing the Admitted warning when running "make check-admitted"
-rw-r--r--mppa_k1c/ExtValues.v2
1 files changed, 1 insertions, 1 deletions
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,