diff options
Diffstat (limited to 'driver/Interp.ml')
| -rw-r--r-- | driver/Interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index a6841460..3fae70e9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -20,7 +20,7 @@ open Values open Memory open Globalenvs open Events -open Ctypes +open !Ctypes open Csyntax open Csem |