Merge PR #12652: Fix erroneous implicits-in-term warning

Reviewed-by: ejgallego
Reviewed-by: herbelin

2 files changed, 17 insertions, 8 deletions

diff --git a/test-suite/bugs/closed/bug_12651.v b/test-suite/bugs/closed/bug_12651.v
new file mode 100644
index 0000000000..cdeeb84912
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12651.v
@@ -0,0 +1,6 @@
+
+Set Warnings "+implicits-in-term".
+Definition thing1 : forall {A}, A -> A := fun A a => a.
+Check thing1 : _ -> _.
+Fail Definition thing2 : forall {A}, A -> A := fun [A] a => a.
+Fail Definition thing2 : forall A, A -> A := fun {A} a => a.
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b9ed4f838d..5ee847a17e 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -29,14 +29,17 @@ let warn_implicits_in_term =
 
 let check_imps ~impsty ~impsbody =
   let rec aux impsty impsbody =
-  match impsty, impsbody with
-  | a1 :: impsty, a2 :: impsbody ->
-    (match a1.CAst.v, a2.CAst.v with
-    | None , None -> aux impsty impsbody
-    | Some _ , Some _ -> aux impsty impsbody
-    | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ())
-  | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
-  | [], [] -> () in
+    match impsty, impsbody with
+    | a1 :: impsty, a2 :: impsbody ->
+      let () = match a1.CAst.v, a2.CAst.v with
+        | None , None | Some _, None -> ()
+        | Some (_,b1) , Some (_,b2) ->
+          if not ((b1:bool) = b2) then warn_implicits_in_term ?loc:a2.CAst.loc ()
+        | None, Some _ -> warn_implicits_in_term ?loc:a2.CAst.loc ()
+      in
+      aux impsty impsbody
+    | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
+    | [], [] -> () in
   aux impsty impsbody
 
 let protect_pattern_in_binder bl c ctypopt =