diff options
| author | Pierre-Marie Pédrot | 2021-04-19 12:05:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-19 12:05:38 +0200 |
| commit | 9d3ea20fb8e9f1c3acfa3d127a1e3ee99fe7ebc9 (patch) | |
| tree | bf7a761119e9309d2da0840a1edc0e10882e515e | |
| parent | 9fe4108289f584461b5dc7af08095d6279a222af (diff) | |
Slightly tweak the not-unit Ltac2 warning.
Fixes #11683.
| -rw-r--r-- | user-contrib/Ltac2/tac2intern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |