Commit 1f36e734 authored by Robbert Krebbers's avatar Robbert Krebbers

Better error message when the argument of iSpecialize is not a hypothesis.

parent 4b2f81cc
......@@ -338,15 +338,19 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
end in
lazymatch t with
| ITrm ?H ?xs ?pat =>
lazymatch p with
| true =>
eapply tac_specialize_persistent_helper with _ H _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H "not found"
|iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
|let Q := match goal with |- PersistentP ?Q => Q end in
apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity|tac H]
| false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
lazymatch type of H with
| string =>
lazymatch p with
| true =>
eapply tac_specialize_persistent_helper with _ H _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H "not found"
|iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
|let Q := match goal with |- PersistentP ?Q => Q end in
apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity|tac H]
| false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
end
| _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
end
end.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment