diff options
Diffstat (limited to 'common/DebugPrint.ml')
| -rw-r--r-- | common/DebugPrint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml index 021ea5c0..d94b31d8 100644 --- a/common/DebugPrint.ml +++ b/common/DebugPrint.ml @@ -1,7 +1,7 @@ open Maps open Camlcoq open Registers -open AuxTools +open RTLcommonaux let debug_flag = ref false |