diff options
| author | Hugo Herbelin | 2018-10-16 15:28:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-31 18:22:41 +0100 |
| commit | ba110aab290cecc8847f3bc3b8396d5d1b9493b0 (patch) | |
| tree | aa5908c85f85997bbe03423826ad512ea14761b2 /interp | |
| parent | 2a93216a3851688dd29c06a29c6d1442898faab8 (diff) | |
Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).
We compute the binding to tactic-in-term once for all in the right
scopes before interpreting the tactic.
An alternative would have been to surround the constr_expr by
CDelimiters to simulate its interpretation in the expected scopes
(though this would not have worked for temporary scopes).
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c03a5fee90..ac2f82e8ce 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -737,7 +737,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in try let gc = intern nenv c in - Id.Map.add id (gc, Some c) map + Id.Map.add id (gc, None) map with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = |