aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-08-05 14:18:08 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-08-05 16:52:13 +0200
commite329ddbce4917f4cb90e038ed244698713f8f941 (patch)
treeefc70b48c97739bf7f715bb8856a55a14a851fd3
parentd32bd531b00ee8916a003c0b62029ddffbccc35b (diff)
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].
-rw-r--r--tactics/tacinterp.ml13
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;