diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_3468.v | 29 |
2 files changed, 30 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))) = diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v new file mode 100644 index 0000000000..6ff394bca6 --- /dev/null +++ b/test-suite/bugs/closed/bug_3468.v @@ -0,0 +1,29 @@ +(* Checking that unrelated terms requiring some scope do not affect + the interpretation of tactic-in-term. The "Check" was failing with: + The term "Set" has type "Type" while it is expected to have type + "nat". *) + +Notation bar2 a b := (let __ := ltac:(exact I) in (a + b)%type) (only parsing). +Check bar2 (Set + Set) Set. + +(* Taking into account scopes in notations containing tactic-in-term *) + +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Notation "x ~~" := (x) (at level 0, only parsing) : foo_scope. +Notation bar x := (x%foo) (only parsing). +Notation baz x := ltac:(exact x%foo) (only parsing). +Check bar (O ~~). +Check baz (O ~~). (* Was failing *) + +(* This was reported as bug #8706 *) + +Declare Scope my_scope. +Notation "@ a" := a%nat (at level 100, only parsing) : my_scope. +Delimit Scope my_scope with my. + +Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope. +Definition test := (& (@4))%my. + +(* Check inconsistent scopes *) +Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing). |