From 2aa6cd0cc6bf7cecdc910e538107598895bbf633 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 15 Feb 2017 20:31:35 +0100 Subject: [PATCH] Make (e)auto enter proofmode when we are not already in it. --- theories/proofmode/tactics.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index f329c4624..7ebf8bcbd 100644 --- a/theories/proofmode/tactics.v +++ b/theories/proofmode/tactics.v @@ -1407,9 +1407,12 @@ Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) := (* Make sure that by and done solve trivial things in proof mode *) Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro. Hint Extern 0 (of_envs _ ⊢ _) => iAssumption. -Hint Extern 0 (of_envs _ ⊢ _) => progress iIntros. Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *) +(* For iIntros we do not check whether we are in proof mode because we actually +want it to enter proof mode when we are not already in it. *) +Hint Extern 0 (_ ⊢ _) => progress iIntros. + Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit. Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit. Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext. @@ -1420,4 +1423,4 @@ Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro. Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft. Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight. -Hint Extern 2 (coq_tactics.of_envs _ ⊢ _ ∗ _) => progress iFrame : iFrame. +Hint Extern 2 (of_envs _ ⊢ _ ∗ _) => progress iFrame : iFrame. -- GitLab