diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-02-27 17:12:42 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-02-27 17:12:42 -0500 |
| commit | 33f32edf2278232a5236181514aa9836b024450b (patch) | |
| tree | 8c3d715fe4fe53415cd8848a1eacbf42112de4f3 /src | |
| parent | 61911f8a41a264c9066f9e145597157b3ebf6a79 (diff) | |
Update a proof to work with previous commit
Diffstat (limited to 'src')
| -rw-r--r-- | src/UnderLetsProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 72c3ff53d..41bf801d2 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -351,9 +351,9 @@ Module Compilers. Lemma interp_splice_list {A B} (x : list (UnderLets A)) (e : list A -> UnderLets B) : interp (splice_list x e) - = interp (e (map interp x)). + = interp (e (List.map interp x)). Proof. - revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp map]; [ reflexivity | ]. + revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp List.map]; [ reflexivity | ]. rewrite interp_splice, IHx; reflexivity. Qed. |