diff options
| author | SimonBoulier | 2020-01-07 10:07:08 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-01-07 10:11:21 +0100 |
| commit | 751ad4098768569450306b7e269081bbac81ea71 (patch) | |
| tree | cb2cdaa2b57736cc0d9c99b4ed381b33d2d039a5 | |
| parent | 793bddef6b4f615297e9f9088cd0b603c56b2014 (diff) | |
Turn trailing implicit warning into an error
| -rw-r--r-- | interp/impargs.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index df28b32f81..b22407c2b7 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -648,9 +648,8 @@ let maybe_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 +661,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" |