diff options
Diffstat (limited to 'backend/Stackingtyping.v')
| -rw-r--r-- | backend/Stackingtyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index b88dd50..1bafc35 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -51,7 +51,7 @@ Variable tf: Mach.function. Hypothesis TRANSF_F: transf_function f = OK tf. Lemma wt_fold_right: - forall (A: Set) (f: A -> code -> code) (k: code) (l: list A), + forall (A: Type) (f: A -> code -> code) (k: code) (l: list A), (forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) -> wt_instrs k -> wt_instrs (List.fold_right f k l). |