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

13 files changed, 35 insertions, 34 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1a81dc41a1..622a9aee3d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2437,7 +2437,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
               let impls =
 		if k == Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
-		    (ExplByPos (n, na), (true, true, true)) :: impls
+                    CAst.make (ExplByPos (n, na), (true, true, true)) :: impls
 		else impls
 	      in
                 (push_rel d env, sigma, d::params, succ n, impls)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d4bc91f57..4bf8ee9429 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -61,10 +61,10 @@ type internalization_env = var_internalization_data Id.Map.t
 val empty_internalization_env : internalization_env
 
 val compute_internalization_data : env -> evar_map -> var_internalization_type ->
-  types -> Impargs.manual_explicitation list -> var_internalization_data
+  types -> Impargs.manual_implicits -> var_internalization_data
 
 val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type ->
-  Id.t list -> types list -> Impargs.manual_explicitation list list ->
+  Id.t list -> types list -> Impargs.manual_implicits list ->
   internalization_env
 
 type ltac_sign = {
diff --git a/interp/impargs.ml b/interp/impargs.ml
index f3cdd64633..81fe3e22b3 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -369,6 +369,7 @@ let check_correct_manual_implicits autoimps l =
 
 (* Take a list l of explicitations, and map them to positions. *)
 let flatten_explicitations l autoimps =
+  let l = List.map (fun c -> c.CAst.v) l in
   let rec aux k l = function
     | (Name id,_)::imps ->
        let value, l' =
@@ -644,7 +645,7 @@ let declare_mib_implicits kn =
 (* Declare manual implicits *)
 type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
 
-type manual_implicits = manual_explicitation list
+type manual_implicits = manual_explicitation CAst.t list
 
 let compute_implicits_with_manual env sigma typ enriching l =
   let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
@@ -669,8 +670,8 @@ let projection_implicits env p impls =
   CList.skipn_at_least npars impls
 
 let declare_manual_implicits local ref ?enriching l =
-  assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l);
-  assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l);
+  assert (List.for_all (fun {CAst.v=(_, (max, fi, fu))} -> fi && fu) l);
+  assert (List.for_all (fun {CAst.v=(ex, _)} -> match ex with ExplByPos (_,_) -> true | _ -> false) l);
   let flags = !implicit_args in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -751,10 +752,10 @@ let extract_impargs_data impls =
   aux 0 impls
 
 let lift_implicits n =
-  List.map (fun x ->
+  List.map (CAst.map (fun x ->
     match fst x with
 	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
-      | _ -> x)
+      | _ -> x))
 
 let make_implicits_list l = [DefaultImpArgs, l]
 
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1099074c63..07f015d319 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -90,7 +90,7 @@ val positions_of_implicits : implicits_list -> int list
 type manual_explicitation = Constrexpr.explicitation *
     (maximal_insertion * force_inference * bool)
 
-type manual_implicits = manual_explicitation list
+type manual_implicits = manual_explicitation CAst.t list
 
 val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool ->
   manual_implicits -> implicit_status list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bac46c2d2f..34674fb102 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -257,19 +257,19 @@ let warn_ignoring_implicit_status =
        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
+  let add_impl ?loc i na bk l = match bk with
   | Implicit ->
     let name =
       match na with
       | Name id -> Some id
       | Anonymous -> None
     in
-    (ExplByPos (i, name), (true, true, true)) :: l
+    CAst.make ?loc (ExplByPos (i, name), (true, true, true)) :: l
   | _ -> l
   in
   let rec aux i c =
-    let abs na bk b =
-      add_impl i na bk (aux (succ i) b)
+    let abs ?loc na bk b =
+      add_impl ?loc i na bk (aux (succ i) b)
     in
     match DAst.get c with
     | GProd (na, bk, t, b) ->
@@ -279,10 +279,10 @@ let implicits_of_glob_constr ?(with_products=true) l =
           | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
           | _ -> ()
         in []
-    | GLambda (na, bk, t, b) -> abs na bk b
+    | GLambda (na, bk, t, b) -> abs ?loc:t.CAst.loc na bk b
     | GLetIn (na, b, t, c) -> aux i c
     | 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)
+      List.fold_left_i (fun i l (na,bk,t,_) -> add_impl ?loc:c.CAst.loc i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
     | _ -> []
   in aux 1 l
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