diff options
Diffstat (limited to 'backend/RTLgenaux.ml')
| -rw-r--r-- | backend/RTLgenaux.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 045299d4..e39d3b56 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -11,9 +11,7 @@ (* *********************************************************************) open Datatypes -open Camlcoq open AST -open Switch open CminorSel (* Heuristic to orient if-then-else statements. |