diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-06 18:01:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-06 18:01:58 +0200 |
| commit | e9c6d4cbc9973e0c46b8022fcc5a794f363d1e86 (patch) | |
| tree | c5b06886c87392ac9c976a7773a7bc0c219bc17a /interp | |
| parent | 49b30563c4c2d5e967912c96d2e34d9e81a1e675 (diff) | |
| parent | 350044bcfb809ef73c3a76a820641da7480b3c9e (diff) | |
Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provide line number
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a1a3be70f..58df9abc4 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -245,6 +245,12 @@ let implicit_application env ?(allow_partial=true) f ty = CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid in c, avoid +let warn_ignoring_implicit_status = + CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" + (fun na -> + strbrk "Ignoring implicit status of product binder " ++ + Name.print na ++ strbrk " and following binders") + let implicits_of_glob_constr ?(with_products=true) l = let add_impl i na bk l = match bk with | Implicit -> @@ -260,20 +266,18 @@ let implicits_of_glob_constr ?(with_products=true) l = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match DAst.get c with - | GProd (na, bk, t, b) -> - if with_products then abs na bk b - else - let () = match bk with - | Implicit -> - Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - Name.print na ++ strbrk " and following binders") - | _ -> () - in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b - | GRec (fix_kind, nas, args, tys, bds) -> - let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) - | _ -> [] + match DAst.get c with + | GProd (na, bk, t, b) -> + if with_products then abs na bk b + else + let () = match bk with + | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | _ -> () + in [] + | GLambda (na, bk, t, b) -> abs na bk b + | GLetIn (na, b, t, c) -> aux i b + | GRec (fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + | _ -> [] in aux 1 l |