From 9fe7c0b44d9405d4008210d674aa742b2d343c4a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Oct 2019 11:12:21 +0200
Subject: Fixes #10894: uconstr was not anymore typed in the Ltac-substituted
 environment.

More precisely: The equivalent in #7288 (4dab4fc) to the former call
to ltac_interp_name_env was not done anymore when interpreting
uconstr's.
---
 pretyping/globEnv.ml               |  2 +-
 test-suite/bugs/closed/bug_10894.v | 12 ++++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_10894.v

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index d49a39b547..aebe47a7a7 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -166,7 +166,7 @@ let interp_ltac_variable ?loc typing_fun env sigma id : Evd.evar_map * unsafe_ju
        here, as the call to the main pretyping function is caught
        inside the try but I want to avoid refactoring this function
        too much for now. *)
-    typing_fun {env with lvar} term
+    typing_fun {env with lvar; static_env = env.renamed_env} term
   with Not_found ->
   (* Check if [id] is a ltac variable not bound to a term *)
   (* and build a nice error message *)
diff --git a/test-suite/bugs/closed/bug_10894.v b/test-suite/bugs/closed/bug_10894.v
new file mode 100644
index 0000000000..b8c9367951
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10894.v
@@ -0,0 +1,12 @@
+(* Check that uconstrs are interpreted in the ltac-substituted environment *)
+(* Was a regression introduced in 4dab4fc (#7288) *)
+
+Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) :=
+   set (h := fun x => f).
+
+Fact test : nat -> nat.
+Proof.
+  intros n.
+  bind n in (n*n) as f.
+  assert (f 0 = 0) by reflexivity.
+Abort.
-- 
cgit v1.2.3


From e9497e5131f13cdea86aff8ae697415d400538fd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Oct 2019 14:47:44 +0200
Subject: Adding changelog

---
 .../10899-master+fix10894-regression-ltac-uconstr-typing.rst             | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst

diff --git a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst b/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst
new file mode 100644
index 0000000000..9d15b7126f
--- /dev/null
+++ b/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst
@@ -0,0 +1 @@
+- Fixed bug #10894: Ltac1 regression in binding free names in uconstr (`#10899 <https://github.com/coq/coq/pull/10899>`_, by Hugo Herbelin).
-- 
cgit v1.2.3