diff options
| -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 = |