diff options
| author | Hugo Herbelin | 2015-10-11 15:05:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-11 15:21:33 +0200 |
| commit | ae5305a4837cce3c7fd61b92ce8110ac66ec2750 (patch) | |
| tree | 3026a62e18044a3126521c0c72eefe8304184262 /pretyping | |
| parent | 2e07ecfce221840047b2f95c93acdb79a4fe0985 (diff) | |
Refining 0c320e79ba30 in fixing interpretation of constr under binders
which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).
Interpretation was corrected, but error message was damaged.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
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 ++ |