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

5 files changed, 16 insertions, 15 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