From a7e12146a95b65ecfc3f1e58d9c76952a599dff5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 13 Nov 2023 16:53:42 +0100 Subject: [PATCH] Ltac2: turn record "the with clause is useless" error into warning (default error) Useless `with` can be useful for compatibility. --- plugins/ltac2/tac2intern.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index ca1269935184..5e4894f21dc4 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1072,6 +1072,12 @@ let tycon_app ?loc env ~ft t = Pp.(str "This expression has type" ++ spc() ++ pr_glbtype env ft ++ str"." ++ spc() ++ str "It is not a function and cannot be applied.") +let warn_useless_record_with = CWarnings.create ~name:"ltac2-useless-record-with" ~default:AsError + ~category:CWarnings.CoreCategories.ltac2 + Pp.(fun () -> + str "All the fields are explicitly listed in this record:" ++ + spc() ++ str "the 'with' clause is useless.") + let rec intern_rec env tycon {loc;v=e} = let check et = check ?loc env tycon et in match e with @@ -1225,10 +1231,7 @@ let rec intern_rec env tycon {loc;v=e} = MissingField i) args in - let () = if not !used then - user_err ?loc (str "All the fields are explicitly listed in this record:" ++ - spc() ++ str "the 'with' clause is useless."); - in + let () = if not !used then warn_useless_record_with ?loc (); in let def = intern_rec_with_constraint env def (GTypRef (Other kn, Array.to_list deftparam)) in let var = match def with | GTacVar _ | GTacRef _ -> None