From ae327e1f044f28593a82b8b2ed181d0734f99df2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 22 Dec 2018 11:48:43 +0100
Subject: [PATCH] Remove spurious spaces in proof mode error messages.
---
theories/proofmode/ltac_tactics.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 096e1a737..c35f5c6fa 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1043,7 +1043,7 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
|pm_reflexivity ||
let H1 := pretty_ident H1 in
let H2 := pretty_ident H2 in
- fail "iAndDestruct:" H1 "or" H2 " not fresh"
+ fail "iAndDestruct:" H1 "or" H2 "not fresh"
|(* subgoal *)].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
@@ -1054,7 +1054,7 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
fail "iAndDestructChoice: cannot destruct" P
|pm_reflexivity ||
let H' := pretty_ident H' in
- fail "iAndDestructChoice:" H' " not fresh"
+ fail "iAndDestructChoice:" H' "not fresh"
|(* subgoal *)].
(** * Existential *)
@@ -1141,7 +1141,7 @@ Tactic Notation "iModCore" constr(H) :=
|iSolveTC ||
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
- fail "iMod: cannot eliminate modality " P "in" Q
+ fail "iMod: cannot eliminate modality" P "in" Q
|iSolveSideCondition
|pm_reflexivity
|(* subgoal *)].
@@ -2166,7 +2166,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
end;
[iSolveTC ||
let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in
- fail "iInv: cannot eliminate invariant " I
+ fail "iInv: cannot eliminate invariant" I
|iSolveSideCondition
|let R := fresh in intros R; eexists; split; [pm_reflexivity|];
(* Now we are left proving [envs_entails Δ'' R]. *)
--
GitLab