Commit 730f24ec authored by Ralf Jung's avatar Ralf Jung
Browse files

slightly extend iPureIntro automation comment

parent 004f161f
......@@ -3325,7 +3325,9 @@ Tactic Notation "iAccu" :=
Global Hint Extern 0 (_ _) => iStartProof : core.
Global Hint Extern 0 ( _) => iStartProof : core.
(* Make sure that by and done solve trivial things in proof mode *)
(* Make sure that [by] and [done] solve trivial things in proof mode.
[iPureIntro] invokes [FromPure], so adding [FromPure] instances can help improve
what [done] can do. *)
Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
Global Hint Extern 0 (envs_entails _ ?Q) =>
first [is_evar Q; fail 1|iAssumption] : core.
......
Supports Markdown
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