ltac_tactics.v: drop dead branch

parent fd192eff
......@@ -1027,13 +1027,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end in
lazymatch type of t with
| ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
| _ =>
lazymatch eval compute in lazy_tc with
| true =>
iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
| false =>
iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
end
| _ => iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
end.
(** * The apply tactic *)
......
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