diff options
| author | Hugo Herbelin | 2020-01-19 19:11:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-19 19:11:58 +0100 |
| commit | 2ae084f55c2e9bce3023a25a1e2c7a70dadcf348 (patch) | |
| tree | 9a3b7a26e79d80764533ce9618d03a0eb35347f5 /interp | |
| parent | c4de7eb4a4e470864ecd06bb240a3f572d7d84d7 (diff) | |
| parent | b9f3e03dd07e678ce900f332cf4653c5d222ee16 (diff) | |
Merge PR #11368: Turn trailing implicit warning into an error
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/impargs.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index df28b32f81..e2c732809a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -646,11 +646,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l -(* TODO: either turn these warnings on and document them, or handle these cases sensibly *) -let warn_set_maximal_deprecated = - CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated" - (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal")) +let msg_trailing_implicit id = + user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].")) type implicit_kind = Implicit | MaximallyImplicit | NotImplicit @@ -662,7 +660,7 @@ let compute_implicit_statuses autoimps l = | Name id :: autoimps, Implicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality imps' false in - if max then warn_set_maximal_deprecated i; + if max then msg_trailing_implicit id; Some (ExplByName id, Manual, (max, true)) :: imps' | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> user_err ~hdr:"set_implicits" |