aboutsummaryrefslogtreecommitdiffstats
path: root/caml/Allocationaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'caml/Allocationaux.ml')
-rw-r--r--caml/Allocationaux.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/caml/Allocationaux.ml b/caml/Allocationaux.ml
index 8e4f3284..c682c3c1 100644
--- a/caml/Allocationaux.ml
+++ b/caml/Allocationaux.ml
@@ -1,6 +1,6 @@
open Camlcoq
open Datatypes
-open List
+open CList
open AST
open Locations
@@ -36,4 +36,4 @@ let parallel_move_order lsrc ldst =
for i = 0 to n - 1 do
if status.(i) = To_move then move_one i
done;
- List.rev !moves
+ CList.rev !moves