From adc223385c7aa8b43761f4ebb102b4b7b1241123 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Mar 2021 12:06:51 +0200
Subject: Print type of offending expression in Ltac2 not-unit warning.

Partial fix of #14013.
---
 user-contrib/Ltac2/tac2intern.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 90c8528203..206f4df19d 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -467,7 +467,9 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
 
 let warn_not_unit =
   CWarnings.create ~name:"not-unit" ~category:"ltac"
-    (fun () -> strbrk "The following expression should have type unit.")
+    (fun (env, t) ->
+      strbrk "The following expression should have type unit but has type " ++
+      pr_glbtype env t ++ str ".")
 
 let warn_redundant_clause =
   CWarnings.create ~name:"redundant-clause" ~category:"ltac"
@@ -480,7 +482,7 @@ let check_elt_unit loc env t =
   | GTypRef (Tuple 0, []) -> true
   | GTypRef _ -> false
   in
-  if not maybe_unit then warn_not_unit ?loc ()
+  if not maybe_unit then warn_not_unit ?loc (env, t)
 
 let check_elt_empty loc env t = match kind env t with
 | GTypVar _ ->
@@ -504,7 +506,7 @@ let check_unit ?loc t =
   | GTypRef (Tuple 0, []) -> true
   | GTypRef _ -> false
   in
-  if not maybe_unit then warn_not_unit ?loc ()
+  if not maybe_unit then warn_not_unit ?loc (env, t)
 
 let check_redundant_clause = function
 | [] -> ()
-- 
cgit v1.2.3