aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-15 11:12:40 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-15 11:12:40 +0200
commit28557d104a06e001d7f4c9c51ad28abae5beadff (patch)
treeaaa783036efc685925965b86300b76020b4ecf50
parent0b9b2e75d76a5871345f68af478d3cf4c14395ee (diff)
downloadcompcert-kvx-28557d104a06e001d7f4c9c51ad28abae5beadff.tar.gz
compcert-kvx-28557d104a06e001d7f4c9c51ad28abae5beadff.zip
detail
-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 13d63610..980e18f8 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -576,4 +576,4 @@ Proof.
all: omega.
}
}
-Qed. \ No newline at end of file
+Qed.