summaryrefslogtreecommitdiff
path: root/backend/LTLintyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/LTLintyping.v')
-rw-r--r--backend/LTLintyping.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 1a20f73..e9cc2df 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -122,4 +122,4 @@ Inductive wt_fundef: fundef -> Prop :=
wt_fundef (Internal f).
Definition wt_program (p: program): Prop :=
- forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+ forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.