aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/ExtValues.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/ExtValues.v')
-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 8e00dc99..3529a36f 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -180,4 +180,4 @@ Proof.
{ apply Z_div_pos; omega. }
pose proof modulus_fits_64.
omega.
-Qed. \ No newline at end of file
+Qed.