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/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

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
-- 
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/comAssumption.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index c1f676b043..a27c08d176 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -283,8 +283,8 @@ let context poly l =
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
       status
     else
-      let test {CAst.v = (x, _)} = match x with
-      | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
+      let test x = match x.CAst.v with
+      | Some (Name id',_) -> Id.equal id id'
       | _ -> false
       in
       let impl = List.exists test impls in
-- 
cgit v1.2.3