From e4110b8ef96207da48c62c4ab1c868ae613761d2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 4 Mar 2018 16:12:23 +0100
Subject: [PATCH] Typo.

---
 theories/proofmode/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5f2651d62..6dbaf950b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1937,7 +1937,7 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
    iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
 
 Tactic Notation "iAccu" :=
-  iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar."].
+  iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar"].
 
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 
-- 
GitLab