diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2intern.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2intern.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index 90c8528203..0171ddfcf8 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 "This 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 | [] -> () |