diff options
Diffstat (limited to 'backend/PrintRTL.ml')
| -rw-r--r-- | backend/PrintRTL.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index f2242c13..ba336b0a 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -17,10 +17,8 @@ open Camlcoq open Datatypes open Maps open AST -open Integers open RTL open PrintAST -open PrintOp (* Printing of RTL code *) |