diff options
| -rw-r--r-- | backend/Inliningaux.ml | 2 | ||||
| -rw-r--r-- | backend/PrintCminor.ml | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 2 | ||||
| -rw-r--r-- | driver/Interp.ml | 4 | ||||
| -rw-r--r-- | riscV/Asmexpand.ml | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 842e0c93..2e83eb0c 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -16,7 +16,7 @@ open FSetAVL open Maps open Op open Ordered -open !RTL +open! RTL module PSet = Make(OrderedPositive) diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index b77c5645..c9a6d399 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -16,7 +16,7 @@ (** Pretty-printer for Cminor *) open Format -open !Camlcoq +open! Camlcoq open Integers open AST open PrintAST diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 3dbb9d45..9aa6761c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -21,7 +21,7 @@ open Machine open Cabs open C open Diagnostics -open !Cutil +open! Cutil (** * Utility functions *) diff --git a/driver/Interp.ml b/driver/Interp.ml index 3fae70e9..d4286779 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -15,12 +15,12 @@ open Format open Camlcoq open AST -open !Integers +open! Integers open Values open Memory open Globalenvs open Events -open !Ctypes +open! Ctypes open Csyntax open Csem diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 1df63308..d36b6230 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -23,7 +23,7 @@ open Asm open Asmexpandaux open AST open Camlcoq -open !Integers +open! Integers exception Error of string |