From 4b4ae1345858070a96b70d7d6c043d0ff9f5a4a7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 13:27:43 +0100
Subject: Locating the Ill-typed evar instance error.

Even though it is not strongly supposed to be raised.
---
 pretyping/evarsolve.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..de41c8f22f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -810,7 +810,8 @@ let check_evar_instance unify flags env evd evk1 body =
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
     try Retyping.get_type_of ~lax:true evenv evd body
-    with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
+    with Retyping.RetypeError _ ->
+      let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance"))
   in
   match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd
-- 
cgit v1.2.3


From 6ae29940af487e03ef2eafc9cb5c9b0d015c6a7c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 13:28:41 +0100
Subject: Fixes #12348: long-standing de Bruijn indices bug in imitation
 (solve_simple_eqn).

The bug was that an assumption could be interpreted as a local
definition and wrongly expanded.

It triggered rarely because it involved mixing let-ins and
local assumptions + imitation under binders.
---
 pretyping/evarsolve.ml             |  2 +-
 test-suite/bugs/closed/bug_12348.v | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_12348.v

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de41c8f22f..c58ebe1bbd 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1576,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs
     match EConstr.kind !evdref t with
     | Rel i when i>k ->
         let open Context.Rel.Declaration in
-        (match Environ.lookup_rel (i-k) env' with
+        (match Environ.lookup_rel i env' with
         | LocalAssum _ -> project_variable (RelAlias (i-k))
         | LocalDef (_,b,_) ->
           try project_variable (RelAlias (i-k))
diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v
new file mode 100644
index 0000000000..93ba6f17e0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12348.v
@@ -0,0 +1,11 @@
+(* Was raising an anomaly before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := _ in
+      (fun n : nat => 0 : X) : _.
+
+(* Was raising an ill-typed instance error before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := true in
+      (fun n : nat => 0 : X) : _.
-- 
cgit v1.2.3


From 603023b3e65fe362d0287f9fc6e986ec9ef16684 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 13:52:12 +0100
Subject: Add changelog for #13387.

---
 .../13387-master+fix12348-debruijn-bug-imitation.rst                | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst

diff --git a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst
new file mode 100644
index 0000000000..eaf049dc97
--- /dev/null
+++ b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  A bug producing ill-typed instances of existential variables when let-ins
+  interleaved with assumptions
+  (`#13387 <https://github.com/coq/coq/pull/13387>`_,
+  fixes `#12348 <https://github.com/coq/coq/issues/13387>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3