diff options
Diffstat (limited to 'backend/Machtyping.v')
| -rw-r--r-- | backend/Machtyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 2d8c83d..b9d8009 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -111,4 +111,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. |