Adding location in warning telling implicit arguments differ in term and type.

8 files changed, 19 insertions, 19 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 591e4b130f..c1f676b043 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -283,7 +283,7 @@ let context poly l =
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
       status
     else
-      let test (x, _) = match x with
+      let test {CAst.v = (x, _)} = match x with
       | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
       | _ -> false
       in
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
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a31f3c34e0..1ded9f3d29 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -57,7 +57,7 @@ val interp_recursive :
   (* names / defs / types *)
   (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
   (* ctx per mutual def / implicits / struct annotations *)
-  (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
+  (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Exported for Funind *)
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5bebf955ec..e0f2f05fe3 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -559,8 +559,8 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
   mind
 
 type one_inductive_impls =
-  Impargs.manual_explicitation list (* for inds *)*
-  Impargs.manual_explicitation list list (* for constrs *)
+  Impargs.manual_implicits (* for inds *) *
+  Impargs.manual_implicits list (* for constrs *)
 
 type uniform_inductive_flag =
   | UniformParameters
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index ac647af8b5..25c5b24e91 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -112,7 +112,7 @@ val start_lemma_with_initialization
   -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
   -> (Id.t (* name of thm *) *
      (EConstr.types (* type of thm *) *
-      (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+      (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
   -> int list option
   -> t
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 50d24c20c9..6ef2f80067 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -307,7 +307,7 @@ type program_info_aux = {
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
-  prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
+  prg_implicits : Impargs.manual_implicits;
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 8734d82970..18a7e10733 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -57,7 +57,7 @@ val add_definition
   -> ?term:constr -> types
   -> UState.t
   -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
-  -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+  -> ?implicits:Impargs.manual_implicits
   -> ?kind:Decl_kinds.definition_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
@@ -74,8 +74,7 @@ type fixpoint_kind =
   | IsCoFixpoint
 
 val add_mutual_definitions :
-  (Names.Id.t * constr * types *
-      (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+  (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list ->
   UState.t ->
   ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
   ?tactic:unit Proofview.tactic ->
diff --git a/vernac/record.ml b/vernac/record.ml
index c777ef2c2b..e555c6d154 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -481,7 +481,7 @@ let implicits_of_context ctx =
       match name with
       | Name n -> Some n
       | Anonymous -> None
-    in ExplByPos (i, explname), (true, true, true))
+    in CAst.make (ExplByPos (i, explname), (true, true, true)))
     1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
 let declare_class def cum ubinders univs id idbuild paramimpls params arity