aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-10-17 13:35:49 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2014-10-17 13:35:49 +0200
commit1cf9ccdb5cc84b008ccf51eb81b9cce439c22044 (patch)
treee247aa3c1d507ede7f889e683e80deb306e7c039
parent8f26d2b2820cd30b7de9ce53dfb90bda42d9e401 (diff)
parentd37fb8ea9f824278f058b1a01f272335df3645e3 (diff)
downloadcompcert-1cf9ccdb5cc84b008ccf51eb81b9cce439c22044.tar.gz
compcert-1cf9ccdb5cc84b008ccf51eb81b9cce439c22044.zip
Merge branch 'master' into dwarf
-rw-r--r--checklink/Check.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index f175f16b..c9842f40 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -1,4 +1,3 @@
-open Camlcoq
open Asm
open Asm_printers
open AST