From f95017c2c69ee258ae570b789bce696357d2c365 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 May 2019 15:14:38 +0200
Subject: Adding location in warning telling implicit arguments differ in term
 and type.

---
 vernac/comDefinition.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 1046e354a7..01274e2568 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -27,18 +27,19 @@ let warn_implicits_in_term =
   CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
          (fun () ->
           strbrk "Implicit arguments declaration relies on type." ++ spc () ++
-            strbrk "The term declares more implicits than the type here.")
+            strbrk "Discarding incompatible declaration in term.")
 
 let check_imps ~impsty ~impsbody =
-  let b =
-    try
-      List.for_all (fun (key, (va:bool*bool*bool)) ->
+  let impsty = List.map (fun x -> x.CAst.v) impsty in
+  List.iter (fun {CAst.v = (key, (va:bool*bool*bool)); CAst.loc} ->
+      let b =
+        try
           (* Pervasives.(=) is OK for this type *)
-          Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va)
-        impsbody
-    with Not_found -> false
-  in
-  if not b then warn_implicits_in_term ()
+          Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va
+        with Not_found -> false
+      in
+      if not b then warn_implicits_in_term ?loc ())
+    impsbody
 
 let interp_definition ~program_mode pl bl poly red_option c ctypopt =
   let env = Global.env() in
-- 
cgit v1.2.3


From e034b4090ca45410853db60ae2a5d2f220b48792 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 May 2019 19:21:49 +0200
Subject: Turning "manual_implicits" into a list of position in impargs.ml.

---
 vernac/comDefinition.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 01274e2568..ae1f55acda 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -30,16 +30,16 @@ let warn_implicits_in_term =
             strbrk "Discarding incompatible declaration in term.")
 
 let check_imps ~impsty ~impsbody =
-  let impsty = List.map (fun x -> x.CAst.v) impsty in
-  List.iter (fun {CAst.v = (key, (va:bool*bool*bool)); CAst.loc} ->
-      let b =
-        try
-          (* Pervasives.(=) is OK for this type *)
-          Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va
-        with Not_found -> false
-      in
-      if not b then warn_implicits_in_term ?loc ())
-    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
+  aux impsty impsbody
 
 let interp_definition ~program_mode pl bl poly red_option c ctypopt =
   let env = Global.env() in
@@ -57,11 +57,11 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
     match tyopt with
     | None ->
       let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in
-      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+      evd, c, imps1@impsbody, None
     | Some (ty, impsty) ->
       let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in
       check_imps ~impsty ~impsbody;
-      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+      evd, c, imps1@impsty, Some ty
   in
   (* Do the reduction *)
   let evd, c = red_constant_body red_option env_bl evd c in
-- 
cgit v1.2.3