aboutsummaryrefslogtreecommitdiffstats
path: root/checklink/Check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checklink/Check.ml')
-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