aboutsummaryrefslogtreecommitdiffstats
path: root/caml/RTLgenaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'caml/RTLgenaux.ml')
-rw-r--r--caml/RTLgenaux.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
index d9203808..4c1fc05c 100644
--- a/caml/RTLgenaux.ml
+++ b/caml/RTLgenaux.ml
@@ -28,8 +28,8 @@ module IntSet = Set.Make(IntOrd)
let normalize_table tbl =
let rec norm seen = function
- | CList.Coq_nil -> []
- | CList.Coq_cons(Datatypes.Coq_pair(key, act), rem) ->
+ | [] -> []
+ | Datatypes.Coq_pair(key, act) :: rem ->
if IntSet.mem key seen
then norm seen rem
else (key, act) :: norm (IntSet.add key seen) rem