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.

---
 interp/implicit_quantifiers.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

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
-- 
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.

---
 interp/implicit_quantifiers.ml | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 34674fb102..bab9024415 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -257,32 +257,23 @@ let warn_ignoring_implicit_status =
        Name.print na ++ strbrk " and following binders")
 
 let implicits_of_glob_constr ?(with_products=true) l =
-  let add_impl ?loc i na bk l = match bk with
-  | Implicit ->
-    let name =
-      match na with
-      | Name id -> Some id
-      | Anonymous -> None
-    in
-    CAst.make ?loc (ExplByPos (i, name), (true, true, true)) :: l
-  | _ -> l
+  let add_impl ?loc na bk l = match bk with
+  | Implicit -> CAst.make ?loc (Some (na,true)) :: l
+  | _ -> CAst.make ?loc None :: l
   in
-  let rec aux i c =
-    let abs ?loc na bk b =
-      add_impl ?loc i na bk (aux (succ i) b)
-    in
+  let rec aux c =
     match DAst.get c with
     | GProd (na, bk, t, b) ->
-      if with_products then abs na bk b
+      if with_products then add_impl na bk (aux b)
       else
         let () = match bk with
           | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
           | _ -> ()
         in []
-    | GLambda (na, bk, t, b) -> abs ?loc:t.CAst.loc na bk b
-    | GLetIn (na, b, t, c) -> aux i c
+    | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
+    | GLetIn (na, b, t, c) -> aux 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,t,_) -> add_impl ?loc:c.CAst.loc i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
+      List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb))
     | _ -> []
-  in aux 1 l
+  in aux l
-- 
cgit v1.2.3