Skip to content
Snippets Groups Projects
Commit 29f83cf5 authored by Ralf Jung's avatar Ralf Jung
Browse files

use notypeclasses refine for iInv

parent f53bcfd3
No related branches found
No related tags found
No related merge requests found
...@@ -2948,13 +2948,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H ...@@ -2948,13 +2948,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
end in end in
lazymatch type of select with lazymatch type of select with
| string => | string =>
eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat); notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
[ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..] [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
| ident => | ident =>
eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat); notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
[ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..] [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
| namespace => | namespace =>
eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat); notypeclasses refine (tac_inv_elim _ _ H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
[ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..] [ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..]
| _ => fail "iInv: selector" select "is not of the right type " | _ => fail "iInv: selector" select "is not of the right type "
end; end;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment