diff options
| author | Hugo Herbelin | 2020-08-22 12:48:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 699eb941cbdd2b3caf98f18b2d49b249b598ca1b (patch) | |
| tree | ad1bc6c93d8d914d09724a19561baa1899d4e7b9 /plugins/ssr | |
| parent | 3df82e1adcfb96320b3fbbb622d9e54cb0a176e1 (diff) | |
When reporting an implicit argument error on a rename argument, use the renaming.
Example:
> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 24772a8514..4a907b2795 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -159,7 +159,7 @@ let declare_one_prenex_implicit locality f = | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> - Impargs.set_implicits locality fref [impls] + Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls] } |