aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-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,