aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintCminor.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/PrintCminor.ml')
-rw-r--r--backend/PrintCminor.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 9b6b1488..5e686b55 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -17,7 +17,6 @@
open Format
open Camlcoq
-open Datatypes
open Integers
open AST
open PrintAST
@@ -27,7 +26,7 @@ open Cminor
type associativity = LtoR | RtoL | NA
-let rec precedence = function
+let precedence = function
| Evar _ -> (16, NA)
| Econst _ -> (16, NA)
| Eunop _ -> (15, RtoL)