aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmexpand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'arm/Asmexpand.ml')
-rw-r--r--arm/Asmexpand.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index a4ec0c5d..89aab5c7 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -18,7 +18,7 @@ open Asm
open Asmexpandaux
open AST
open Camlcoq
-open Integers
+open! Integers
exception Error of string