aboutsummaryrefslogtreecommitdiffstats
path: root/backend/IRC.mli
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-21 22:39:27 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-21 22:39:27 +0100
commit23fa2a18e015b9d330ad6f1f08cf50adf90bd80b (patch)
treee3e39eebc5164b967db9b16504bfe19edc4d2bdc /backend/IRC.mli
parentab5528fb4caf637a0c7014d943302198079e7c20 (diff)
downloadcompcert-kvx-23fa2a18e015b9d330ad6f1f08cf50adf90bd80b.tar.gz
compcert-kvx-23fa2a18e015b9d330ad6f1f08cf50adf90bd80b.zip
try to be portable across archs
Diffstat (limited to 'backend/IRC.mli')
-rw-r--r--backend/IRC.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/IRC.mli b/backend/IRC.mli
index 30b6d5c1..f7bbf9c5 100644
--- a/backend/IRC.mli
+++ b/backend/IRC.mli
@@ -43,5 +43,4 @@ val coloring: graph -> (var -> loc)
val reserved_registers: mreg list ref
(* Auxiliaries to deal with register classes *)
-val class_of_type: AST.typ -> int
val class_of_loc: loc -> int