aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLgenaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/RTLgenaux.ml')
-rw-r--r--backend/RTLgenaux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 82cb300f..0822587f 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -29,7 +29,7 @@ module IntSet = Set.Make(IntOrd)
let normalize_table tbl =
let rec norm keys accu = function
| [] -> (accu, keys)
- | Datatypes.Coq_pair(key, act) :: rem ->
+ | (key, act) :: rem ->
if IntSet.mem key keys
then norm keys accu rem
else norm (IntSet.add key keys) ((key, act) :: accu) rem