Fix interpretation bug in [uconstr].

Substitution of the Ltac variables would only occur if the internalised [uconstr] was of the form [glob, Some expr], which is the case only in tactics defined inside a proof, but not in tactics defined in [Ltac].

1 files changed, 11 insertions, 2 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 826846f90..1f53e19c3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -467,9 +467,18 @@ let extract_ltac_uconstr_values ist env =
 
 (** Significantly simpler than [interp_constr], to interpret an
     untyped constr, it suffices to substitute any bound Ltac variables
-    while redoint internalisation. *)
+    while redoing internalisation. *)
+let subst_in_ucconstr subst =
+  let rec subst_in_ucconstr = function
+  | Glob_term.GVar (_,id) as x ->
+      begin try Lazy.force (Id.Map.find id subst)
+      with Not_found -> x end
+  | c -> Glob_ops.map_glob_constr subst_in_ucconstr c
+  in
+  subst_in_ucconstr
+
 let interp_uconstr ist env = function
-  | (c,None) -> c
+  | (c,None) -> subst_in_ucconstr (extract_ltac_uconstr_values ist env) c
   | (_,Some ce) ->
       let ltacvars = {
         Constrintern.ltac_vars = Id.Set.empty;