summaryrefslogtreecommitdiff
path: root/backend/Cminor.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Cminor.v')
-rw-r--r--backend/Cminor.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v
index bdfb379..4e57d3c 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -133,8 +133,8 @@ Definition program := AST.program fundef unit.
Definition funsig (fd: fundef) :=
match fd with
- | Internal f => f.(fn_sig)
- | External ef => ef.(ef_sig)
+ | Internal f => fn_sig f
+ | External ef => ef_sig ef
end.
(** * Operational semantics (small-step) *)