Refining 0c320e79ba30 in fixing interpretation of constr under binders

which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).

Interpretation was corrected, but error message was damaged.

4 files changed, 23 insertions, 2 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6306739b7a..746b4000ee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -322,8 +322,8 @@ let ltac_interp_name_env k0 lvar env =
   push_rel_context ctxt env
 
 let invert_ltac_bound_name lvar env id0 id =
-  let id = Id.Map.find id lvar.ltac_idents in
-  try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+  let id' = Id.Map.find id lvar.ltac_idents in
+  try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
     errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
new file mode 100644
index 0000000000..d003c70df9
--- /dev/null
+++ b/test-suite/output/ltac.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
new file mode 100644
index 0000000000..567e21edbe
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,8 @@
+(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
+Goal True.
+Fail let T := constr:((fun a b : nat => a+b) 1 1) in
+  lazymatch T with
+  | (fun x z => ?y) 1 1
+    => pose ((fun x _ => y) 1 1)
+  end.
+Abort.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index f9df021dc2..6c4d4ae98f 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -306,3 +306,14 @@ let x := ipattern:y in assert (forall x y, x = y + 0).
 intro.
 destruct y. (* Check that the name is y here *)
 Abort.
+
+(* An example suggested by Jason (see #4317) showing the intended semantics *)
+(* Order of binders is reverted because y is just told to depend on x *)
+
+Goal 1=1.
+let T := constr:(fun a b : nat => a) in
+  lazymatch T with
+  | (fun x z => ?y) => pose ((fun x x => y) 2 1)
+  end.
+exact (eq_refl n).
+Qed.