diff options
Diffstat (limited to 'backend/RTLtyping.v')
| -rw-r--r-- | backend/RTLtyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 65506c8..a14e944 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -158,7 +158,7 @@ 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. (** * Type inference *) |