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

(limited to 'interp/constrintern.ml')

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)
-- 
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/constrintern.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 622a9aee3d..e55f66e856 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2435,10 +2435,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
               let r = Retyping.relevance_of_type env sigma t in
               let d = LocalAssum (make_annot na r,t) in
               let impls =
-		if k == Implicit then
-		  let na = match na with Name n -> Some n | Anonymous -> None in
-                    CAst.make (ExplByPos (n, na), (true, true, true)) :: impls
-		else impls
+                if k == Implicit then CAst.make (Some (na,true)) :: impls
+                else CAst.make None :: impls
 	      in
                 (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
@@ -2447,7 +2445,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
               let d = LocalDef (make_annot na r, c, t) in
                 (push_rel d env, sigma, d::params, n, impls))
       (env,sigma,[],k+1,[]) (List.rev bl)
-  in sigma, ((env, par), impls)
+  in sigma, ((env, par), List.rev impls)
 
 let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
   let int_env,bl = intern_context global_level env impl_env params in
-- 
cgit v1.2.3