diff options
Diffstat (limited to 'backend/Duplicateaux.ml')
| -rw-r--r-- | backend/Duplicateaux.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index e8e60a4f..8ca6c6ab 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -23,7 +23,7 @@ open RTL open Maps open Camlcoq open DebugPrint -open AuxTools +open RTLcommonaux let stats_oc = ref None |