diff options
Diffstat (limited to 'src/Compilers/MapCastByDeBruijnInterp.v')
| -rw-r--r-- | src/Compilers/MapCastByDeBruijnInterp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v index ca7330796..9e7454c2a 100644 --- a/src/Compilers/MapCastByDeBruijnInterp.v +++ b/src/Compilers/MapCastByDeBruijnInterp.v @@ -118,7 +118,7 @@ Section language. [ reflexivity | auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } { intro; eapply wf_map_cast with (t := Arrow _ _) (fValues := empty); eauto using PositiveContextOk with typeclass_instances. - { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':= e _); + { eapply (wf_compile (ContextOk:=PositiveContextOk) (make_var':=fun _ => id)) with (e':= e _); [ auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } } |