From e329ddbce4917f4cb90e038ed244698713f8f941 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 14:18:08 +0200
Subject: 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].---
 tactics/tacinterp.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 826846f906..1f53e19c36 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;
-- 
cgit v1.2.3