diff options
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 3930da3..da73b00 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -133,7 +133,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. (** Typing the run-time state. These definitions are used in [Stackingproof]. *) |