aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Reload.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Reload.v')
-rw-r--r--backend/Reload.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Reload.v b/backend/Reload.v
index 31bddcd0..be844b30 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -257,7 +257,7 @@ Definition transf_instr
end.
Definition transf_code (f: LTLin.function) (c: LTLin.code) : code :=
- List.fold_right (transf_instr f) nil c.
+ list_fold_right (transf_instr f) c nil.
Definition transf_function (f: LTLin.function) : function :=
mkfunction