Skip to content

GitLab

Commit 66f8aa36 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

eauto hint for introducing ◇.

parent 070a85d9
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 0 deletions
theories/proofmode/tactics.v
View file @ 66f8aa36
...@@ -1280,6 +1280,7 @@ Hint Extern 1 (of_envs _ ⊢ _) => ...@@ -1280,6 +1280,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
| |- _ ⊢ □ _ => iClear "*"; iAlways | |- _ ⊢ □ _ => iClear "*"; iAlways
| |- _ ⊢ ∃ _, _ => iExists _ | |- _ ⊢ ∃ _, _ => iExists _
| |- _ ⊢ |==> _ => iModIntro | |- _ ⊢ |==> _ => iModIntro
| |- _ ⊢ ◇ _ => iModIntro
end. end.
Hint Extern 1 (of_envs _ ⊢ _) => Hint Extern 1 (of_envs _ ⊢ _) =>
match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end. match goal with |- _ ⊢ (_ ∨ _)%I => iLeft 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