diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-28 18:54:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-28 18:55:53 -0400 |
| commit | 20d1a5816a33568f2fe13e28445396c476a49d27 (patch) | |
| tree | e34a378bd9a499387a74660c40cccea3ee176df6 /src/Reflection/MapCastByDeBruijnInterp.v | |
| parent | 1777daf558ae09e73f88ff85cc7a44f804c49193 (diff) | |
Finish proof of wf_map_cast
After | File Name | Before || Change
---------------------------------------------------------------------
0m20.75s | Total | 0m15.19s || +0m05.56s
---------------------------------------------------------------------
0m19.33s | Reflection/Named/MapCastWf | 0m13.82s || +0m05.50s
0m00.79s | Reflection/MapCastByDeBruijnInterp | 0m00.75s || +0m00.04s
0m00.64s | Reflection/MapCastByDeBruijnWf | 0m00.62s || +0m00.02s
Diffstat (limited to 'src/Reflection/MapCastByDeBruijnInterp.v')
| -rw-r--r-- | src/Reflection/MapCastByDeBruijnInterp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v index add7014ce..0e425886b 100644 --- a/src/Reflection/MapCastByDeBruijnInterp.v +++ b/src/Reflection/MapCastByDeBruijnInterp.v @@ -106,7 +106,7 @@ Section language. { erewrite (interp_compile (ContextOk:=PositiveContextOk)), interp_linearize; [ reflexivity | apply wf_linearize; auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } - { intro; eapply wf_map_cast with (t := Arrow _ _) (oldValues := empty); eauto using PositiveContextOk with typeclass_instances. + { intro; eapply wf_map_cast with (t := Arrow _ _) (fValues := empty); eauto using PositiveContextOk with typeclass_instances. { eapply (wf_compile (ContextOk:=PositiveContextOk)); [ apply wf_linearize; auto | .. | eassumption ]. auto using name_list_unique_DefaultNamesFor. } |