From 350044bcfb809ef73c3a76a820641da7480b3c9e Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 30 Mar 2018 16:58:18 +0200
Subject: Fix #7124: Warning "Ignoring implicit status" does not provide line
 number

---
 interp/implicit_quantifiers.ml | 36 ++++++++++++++++++++----------------
 1 file changed, 20 insertions(+), 16 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3