diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-12 18:54:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-12 18:54:31 +0200 |
| commit | 10e5883fed21f9631e1aa65adb7a7e62a529987f (patch) | |
| tree | f04cfc472e6345585eb5f606e2957fcf0f2740ea /pretyping/pretyping.ml | |
| parent | 75c5e421e91d49eec9cd55c222595d2ef45325d6 (diff) | |
| parent | 26974a4a2301cc7b1188a3f2f29f3d3368eccc0b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping/pretyping.ml')
| -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 17eafb19e..bb21b87d3 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 ++ |