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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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 *)
-- 
cgit v1.2.3