aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/pretyping.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6306739b7a..746b4000ee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -322,8 +322,8 @@ let ltac_interp_name_env k0 lvar env =
push_rel_context ctxt env
let invert_ltac_bound_name lvar env id0 id =
- let id = Id.Map.find id lvar.ltac_idents in
- try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ let id' = Id.Map.find id lvar.ltac_idents in
+ try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
with Not_found ->
errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
str " depends on pattern variable name " ++ pr_id id ++