diff options
| author | coqbot-app[bot] | 2021-04-20 20:55:51 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-20 20:55:51 +0000 |
| commit | 3645c06030ed1266fd4160ec7211b4447731bf13 (patch) | |
| tree | f3ee437a6f9ace297c0be6ade2cd4aae1a4b09a5 | |
| parent | cab7a5ddb906e5cef57d78ba7435e89354f3125b (diff) | |
| parent | 9d3ea20fb8e9f1c3acfa3d127a1e3ee99fe7ebc9 (diff) | |
Merge PR #14133: Slightly tweak the not-unit Ltac2 warning.
Reviewed-by: JasonGross
| -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 = |