diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e25ff99e0..bb30c669f 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -320,7 +320,7 @@ let explain_hole_kind env = function | BinderType Anonymous -> str "the type of this anonymous binder" | ImplicitArg (c,(n,ido)) -> - let id = out_some ido in + let id = Option.get ido in str "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c |