From 9d3ea20fb8e9f1c3acfa3d127a1e3ee99fe7ebc9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Apr 2021 12:05:38 +0200
Subject: Slightly tweak the not-unit Ltac2 warning.

Fixes #11683.
---
 user-contrib/Ltac2/tac2intern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 206f4df19d..0171ddfcf8 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -468,7 +468,7 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
 let warn_not_unit =
   CWarnings.create ~name:"not-unit" ~category:"ltac"
     (fun (env, t) ->
-      strbrk "The following expression should have type unit but has type " ++
+      strbrk "This expression should have type unit but has type " ++
       pr_glbtype env t ++ str ".")
 
 let warn_redundant_clause =
-- 
cgit v1.2.3