michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/elaborator): revert commit ededf4fc6c

Browse source 
The instantiate_all are needed. See issue #457
This commit is contained in:
Leonardo de Moura 2015-03-02 13:00:54 -08:00
parent fdb169b8f3
commit c81762970e
2 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -1586,7 +1586,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
return false;
ps = proof_state(ps, tail(gs), subst, ngen);
} else {
expr new_ptac = ptac;
expr new_ptac = subst.instantiate_all(ptac);
if (auto tac = pre_tactic_to_tactic(new_ptac)) {
try {
proof_state_seq seq = (*tac)(env(), ios(), ps);
@ -1648,7 +1648,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
return;
}
if (auto tac = pre_tactic_to_tactic(*pre_tac)) {
if (auto tac = pre_tactic_to_tactic(subst.instantiate_all(*pre_tac))) {
bool show_failure = true;
try_using(subst, mvar, ps, *pre_tac, *tac, show_failure);
return;

11
tests/lean/hott/457.hlean Normal file
View file

@ -0,0 +1,11 @@
import algebra.group
open eq path_algebra
definition foo {A : Type} (a b c : A) (H₁ : a = c) (H₂ : c = b) : a = b :=
begin
apply concat,
rotate 1,
apply H₂,
apply H₁
end