From 03b166ab98f4f0a5520f0aec36f2132ef7a2fe37 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Tue, 25 Feb 2020 14:21:49 +0100
Subject: [PATCH] Slight update to the documentation of [split_and{!,?}]

---
 theories/tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 4045a47e..2203968c 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -84,9 +84,9 @@ Tactic Notation "etrans" := etransitivity.
 (** Tactics for splitting conjunctions:
 
 - [split_and] : split the goal if is syntactically of the shape [_ âˆ§ _]
-- [split_ands?] : split the goal repeatedly (perhaps zero times) while it is
+- [split_and?] : split the goal repeatedly (perhaps zero times) while it is
   of the shape [_ âˆ§ _].
-- [split_ands!] : works similarly, but at least one split should succeed. In
+- [split_and!] : works similarly, but at least one split should succeed. In
   order to do so, it will head normalize the goal first to possibly expose a
   conjunction.
 
-- 
GitLab